let i, n be Nat; :: thesis: ( i in Seg n implies Mx2Tran (AxialSymmetry (i,n)) is rotation )
set S = Seg n;
set M = Mx2Tran (AxialSymmetry (i,n));
assume A1: i in Seg n ; :: thesis: Mx2Tran (AxialSymmetry (i,n)) is rotation
let p be Point of (TOP-REAL n); :: according to MATRTOP3:def 4 :: thesis: |.p.| = |.((Mx2Tran (AxialSymmetry (i,n))) . p).|
len p = n by CARD_1:def 7;
then A2: i in dom p by A1, FINSEQ_1:def 3;
thus |.((Mx2Tran (AxialSymmetry (i,n))) . p).| = sqrt (Sum (sqr (p +* (i,(- (p . i)))))) by A1, Th10
.= sqrt (((Sum (sqr p)) - ((p . i) ^2)) + ((- (p . i)) ^2)) by A2, Th3
.= |.p.| ; :: thesis: verum