# [isabelle] Proving two real^3 spaces are the same

Hi,
If I have two real^3 spaces S1 and S2 as:
axiomatization
S1 :: "real ^ 2" and
S2 :: "real ^ 2" where
r1: "S1 $ 0 = S2 $ 0" and
r2: "S1 $ 1 = S2 $ 1" and
r3: "S1 $ 2 = S2 $ 2"
lemma "S1 = S2"

`How would one go about proving the lemma? I suppose I'd need Cart_eq, which
``reads:
`
lemma Cart_eq: "(x = y) <--> (ALL i. x$i = y$i)"

`but it quantifies over all i's. Since S1 and S2 have only 3 dimensions,
``then should i be only in the range [1..3]?
`
Thanks
Steve

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*