let n be Nat; :: thesis: for p, q being Point of () st n = 1 & |.p.| = |.q.| holds
ex f being additive homogeneous Function of (),() 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 (); :: thesis: ( n = 1 & |.p.| = |.q.| implies ex f being additive homogeneous Function of (),() 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 (),() 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 (),() st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

take I = id (); :: thesis: ( I is rotation & I . p = q & ( AutMt I = AxialSymmetry (n,n) or AutMt I = 1. (F_Real,n) ) )
id () = Mx2Tran (1. (F_Real,1)) by ;
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 (),() st
( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )

A5: len p = 1 by ;
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 (),() by ;
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
.= sqrt (Sum <*pk*>) by RVSUM_1:55
.= sqrt ((p . 1) ^2) by RVSUM_1:73 ;
A10: len q = 1 by ;
then A11: q = <*(q . 1)*> by FINSEQ_1:40;
|.q.| = sqrt (Sum (sqr <*(q . 1)*>)) by
.= sqrt (Sum <*qk*>) by RVSUM_1:55
.= sqrt ((q . 1) ^2) by RVSUM_1:73 ;
then A12: (q . 1) ^2 = (p . 1) ^2 by ;
len (f . p) = 1 by ;
then f . p = <*((f . p) . 1)*> by FINSEQ_1:40
.= <*(- (p . 1))*> by A1, A7, Th9
.= q by ;
hence ( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) ) by ; :: thesis: verum
end;
end;