let n be Nat; :: thesis:
let p, q be Point of (TOP-REAL n); :: thesis:
set TR = TOP-REAL n;
assume A1: n <> 1 ; :: thesis:
assume A2: |.p.| = |.q.| ; :: thesis:

per cases ;

suppose A3: p = q ; :: thesis:

take I = id (TOP-REAL n); :: thesis:
thus ( I is base_rotation & I . p = q ) by A3, FUNCT_1:17; :: thesis:

end;

suppose A4: p <> q ; :: thesis:

A5: n <> 0

proof

assume A6: n = 0 ; :: thesis:
then p = 0. (TOP-REAL n) by JORDAN2C:105;
hence contradiction by A4, A6, JORDAN2C:105; :: thesis:

end;

then A8: n >= 1 by NAT_1:14;
defpred S₁[ Nat] means ( $1 + 1 <= n implies ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) ex X being set st
( card X = $1 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) ) );
A9: Sum (sqr q) >= 0 by RVSUM_1:86;
A10: card (Seg n) = n by FINSEQ_1:57;
A11: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis:
assume A12: S₁[m] ; :: thesis:
set m1 = m + 1;
assume A13: (m + 1) + 1 <= n ; :: thesis:
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n), Xm being set such that
A14: card Xm = m and
A15: Xm c= Seg n and
A16: for k being Nat st k in Xm holds
(f . p) . k = q . k by A12, NAT_1:13;
set fp = f . p;
set sfp = sqr (f . p);
set sq = sqr q;
A17: m + 1 < n by A13, NAT_1:13;

per cases ;

suppose ex k being Nat st
( k in (Seg n) \ Xm & (sqr (f . p)) . k >= (sqr q) . k ) ; :: thesis:

then consider k being Nat such that
A18: k in (Seg n) \ Xm and
A19: (sqr (f . p)) . k >= (sqr q) . k ;
A20: k in Seg n by A18, XBOOLE_0:def 5;
then A21: 1 <= k by FINSEQ_1:1;
set Xmk = Xm \/ {k};
A22: ( (sqr (f . p)) . k = ((f . p) . k) ^2 & (sqr q) . k = (q . k) ^2 ) by VALUED_1:11;
A23: {k} c= Seg n by A20, ZFMISC_1:31;
then A24: Xm \/ {k} c= Seg n by A15, XBOOLE_1:8;
A25: not k in Xm by A18, XBOOLE_0:def 5;
then card (Xm \/ {k}) = m + 1 by A14, A15, CARD_2:41;
then Xm \/ {k} c< Seg n by A10, A17, A24, XBOOLE_0:def 8;
then consider z being set such that
A26: z in Seg n and
A27: not z in Xm \/ {k} by XBOOLE_0:6;
reconsider z = z as Nat by A26;
A28: 1 <= z by A26, FINSEQ_1:1;
((f . p) . z) ^2 >= 0 by XREAL_1:63;
then A29: 0 + ((q . k) ^2) <= (((f . p) . z) ^2) + (((f . p) . k) ^2) by A19, A22, XREAL_1:7;
A30: z <= n by A26, FINSEQ_1:1;
A31: k <= n by A20, FINSEQ_1:1;
not z in {k} by A27, XBOOLE_0:def 3;
then A32: z <> k by TARSKI:def 1;

now

per cases by A32, XXREAL_0:1;

suppose A33: z < k ; :: thesis:

then consider r being real number such that
A34: ((Mx2Tran (Rotation (z,k,n,r))) . (f . p)) . k = q . k by A28, A29, A31, Th23;
( Mx2Tran (Rotation (z,k,n,r)) is {k,z} -support-yielding & Mx2Tran (Rotation (z,k,n,r)) is base_rotation ) by A28, A31, A33, Th26, Th27;
hence ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k ) by A34; :: thesis:

end;

suppose A35: z > k ; :: thesis:

then consider r being real number such that
A36: ((Mx2Tran (Rotation (k,z,n,r))) . (f . p)) . k = q . k by A21, A29, A30, Th22;
( Mx2Tran (Rotation (k,z,n,r)) is {z,k} -support-yielding & Mx2Tran (Rotation (k,z,n,r)) is base_rotation ) by A21, A30, A35, Th26, Th27;
hence ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k ) by A36; :: thesis:

end;

then consider g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A37: g is {k,z} -support-yielding and
A38: (g . (f . p)) . k = q . k ;
take gf = g * f; :: thesis:
take Xm \/ {k} ; :: thesis:
thus ( card (Xm \/ {k}) = m + 1 & Xm \/ {k} c= Seg n ) by A14, A15, A23, A25, CARD_2:41, XBOOLE_1:8; :: thesis:
let m be Nat; :: thesis:
A39: dom gf = the carrier of (TOP-REAL n) by FUNCT_2:52;
A40: dom g = the carrier of (TOP-REAL n) by FUNCT_2:52;
assume A41: m in Xm \/ {k} ; :: thesis:
then A42: ( m in Xm or m in {k} ) by XBOOLE_0:def 3;

per cases by A42, TARSKI:def 1;

suppose A43: m in Xm ; :: thesis:

then m <> k by A18, XBOOLE_0:def 5;
then not m in {k,z} by A27, A41, TARSKI:def 2;
then (g . (f . p)) . m = (f . p) . m by A37, A40, Def1;
hence (gf . p) . m = (f . p) . m by A39, FUNCT_1:12
.= q . m by A16, A43 ;
:: thesis:

end;

suppose m = k ; :: thesis:

hence (gf . p) . m = q . m by A38, A39, FUNCT_1:12; :: thesis:

end;

suppose A44: for k being Nat st k in (Seg n) \ Xm holds
(sqr (f . p)) . k < (sqr q) . k ; :: thesis:

A45: Sum (sqr (f . p)) >= 0 by RVSUM_1:86;
( Sum (sqr q) >= 0 & |.p.| = |.(f . p).| ) by Def4, RVSUM_1:86;
then A46: Sum (sqr (f . p)) = Sum (sqr q) by A2, A45, SQUARE_1:28;
f . p = @ (@ (f . p)) ;
then A47: len (sqr (f . p)) = len (f . p) by TOPREAL7:8;
q = @ (@ q) ;
then A48: len (sqr q) = len q by TOPREAL7:8;
( len (f . p) = n & len q = n ) by CARD_1:def 7;
then reconsider sfp = sqr (f . p), sq = sqr q as Element of n -tuples_on REAL by A47, A48, FINSEQ_2:92;
m < n by A17, NAT_1:13;
then Xm <> Seg n by A14, FINSEQ_1:57;
then Xm c< Seg n by A15, XBOOLE_0:def 8;
then consider z being set such that
A49: z in Seg n and
A50: not z in Xm by XBOOLE_0:6;
reconsider z = z as Nat by A49;
A51: z in (Seg n) \ Xm by A49, A50, XBOOLE_0:def 5;
for k being Nat st k in Seg n holds
sfp . k <= sq . k

proof

let k be Nat; :: thesis:
assume A52: k in Seg n ; :: thesis:

per cases by A52, XBOOLE_0:def 5;

suppose k in (Seg n) \ Xm ; :: thesis:

hence sfp . k <= sq . k by A44; :: thesis:

end;

suppose k in Xm ; :: thesis:

then (f . p) . k = q . k by A16;
then sfp . k = (q . k) ^2 by VALUED_1:11
.= sq . k by VALUED_1:11 ;
hence sfp . k <= sq . k ; :: thesis:

end;

then sfp . z >= sq . z by A46, A49, RVSUM_1:83;
hence ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) ex X being set st
( card X = m + 1 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) ) by A44, A51; :: thesis:

end;

reconsider n1 = n - 1 as Nat by A5, NAT_1:14, NAT_1:21;
A53: n1 + 1 = n ;
A54: S₁[ 0 ]

proof

assume 0 + 1 <= n ; :: thesis:
take f = id (TOP-REAL n); :: thesis:
take X = {} ; :: thesis:
thus ( card X = 0 & X c= Seg n ) by XBOOLE_1:2; :: thesis:
let k be Nat; :: thesis:
assume k in X ; :: thesis:
hence (f . p) . k = q . k ; :: thesis:

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A54, A11);
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n), X being set such that
A55: ( card X = n1 & X c= Seg n ) and
A56: for k being Nat st k in X holds
(f . p) . k = q . k by A53;
card ((Seg n) \ X) = n - n1 by A10, A55, CARD_2:44;
then consider z being set such that
A57: {z} = (Seg n) \ X by CARD_2:42;
set fp = f . p;
( Sum (sqr (f . p)) >= 0 & |.p.| = |.(f . p).| ) by Def4, RVSUM_1:86;
then A58: Sum (sqr q) = Sum (sqr (f . p)) by A2, A9, SQUARE_1:28;
A59: z in {z} by TARSKI:def 1;
then A60: z in Seg n by A57, XBOOLE_0:def 5;
reconsider z = z as Nat by A57, A59;
set fpz = (f . p) +* (z,(q . z));
A61: len (f . p) = n by CARD_1:def 7;
then A62: dom (f . p) = Seg n by FINSEQ_1:def 3;
A63: for k being Nat st 1 <= k & k <= n holds
((f . p) +* (z,(q . z))) . k = q . k

proof

let k be Nat; :: thesis:
assume ( 1 <= k & k <= n ) ; :: thesis:
then A64: k in Seg n by FINSEQ_1:1;

per cases ;

suppose k = z ; :: thesis:

hence ((f . p) +* (z,(q . z))) . k = q . k by A62, A64, FUNCT_7:31; :: thesis:

end;

suppose A65: k <> z ; :: thesis:

then not k in (Seg n) \ X by A57, TARSKI:def 1;
then A66: k in X by A64, XBOOLE_0:def 5;
((f . p) +* (z,(q . z))) . k = (f . p) . k by A65, FUNCT_7:32;
hence ((f . p) +* (z,(q . z))) . k = q . k by A56, A66; :: thesis:

end;

A67: ( len ((f . p) +* (z,(q . z))) = len (f . p) & len q = n ) by CARD_1:def 7, FUNCT_7:97;
then A68: (f . p) +* (z,(q . z)) = q by A61, A63, FINSEQ_1:14;
then A69: Sum (sqr q) = ((Sum (sqr (f . p))) - (((f . p) . z) ^2)) + ((q . z) ^2) by A60, A62, Th3;

per cases ) . z = q . z or (f . p) . z = - (q . z) ) by A69, A58, SQUARE_1:40;

suppose (f . p) . z = q . z ; :: thesis:

then f . p = q by A68, FUNCT_7:35;
hence ex f being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q ) ; :: thesis:

end;

suppose A70: (f . p) . z = - (q . z) ; :: thesis:

1 < n by A1, A8, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider h being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) such that
A71: h is base_rotation and
A72: h . (f . p) = (f . p) +* (z,(- ((f . p) . z))) by A60, Th33;
dom (h * f) = the carrier of (TOP-REAL n) by FUNCT_2:52;
then (h * f) . p = (f . p) +* (z,(- ((f . p) . z))) by A72, FUNCT_1:12
.= q by A61, A63, A67, A70, FINSEQ_1:14 ;
hence ex f being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q ) by A71; :: thesis:

end;