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) ) )

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 )
;

end;

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) ) )

( 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;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

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) ) )

( 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;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