let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) st n = 1 & |.p.| = |.q.| holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )
let p, q be Point of (TOP-REAL n); :: thesis: ( n = 1 & |.p.| = |.q.| implies ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) ) )
set TR = TOP-REAL n;
assume that
A1: n = 1 and
A2: |.p.| = |.q.| ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

per cases ( p = q or p <> q ) ;

suppose A3: p = q ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

take I = id (TOP-REAL n); :: thesis: ( I is rotation & I . p = q & ( AutMt I = AxialSymmetry (n,n) or AutMt I = 1. (F_Real,n) ) )
id (TOP-REAL n) = Mx2Tran (1. (F_Real,1)) by A1, MATRTOP1:33;
hence ( I is rotation & I . p = q & ( AutMt I = AxialSymmetry (n,n) or AutMt I = 1. (F_Real,n) ) ) by A1, A3, Def6; :: thesis: verum

end;

suppose A4: p <> q ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

A5: len p = 1 by A1, CARD_1:def 7;
then A6: p = <*(p . 1)*> by FINSEQ_1:40;
A7: 1 in Seg 1 ;
then reconsider f = Mx2Tran (AxialSymmetry (1,1)) as additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) by A1, Th27;
take f ; :: thesis: ( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )
A8: ( (q . 1) ^2 >= 0 & (p . 1) ^2 >= 0 ) by XREAL_1:63;
reconsider pk = (p . 1) ^2 , qk = (q . 1) ^2 as Real ;
A9: |.p.| = sqrt (Sum (sqr <*(p . 1)*>)) by A5, FINSEQ_1:40
.= sqrt (Sum <*pk*>) by RVSUM_1:55
.= sqrt ((p . 1) ^2) by RVSUM_1:73 ;
A10: len q = 1 by A1, CARD_1:def 7;
then A11: q = <*(q . 1)*> by FINSEQ_1:40;
|.q.| = sqrt (Sum (sqr <*(q . 1)*>)) by A10, FINSEQ_1:40
.= sqrt (Sum <*qk*>) by RVSUM_1:55
.= sqrt ((q . 1) ^2) by RVSUM_1:73 ;
then A12: (q . 1) ^2 = (p . 1) ^2 by A2, A8, A9, SQUARE_1:28;
len (f . p) = 1 by A1, CARD_1:def 7;
then f . p = <*((f . p) . 1)*> by FINSEQ_1:40
.= <*(- (p . 1))*> by A1, A7, Th9
.= q by A4, A6, A11, A12, SQUARE_1:40 ;
hence ( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) ) by A1, Def6; :: thesis: verum

end;

end;