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; :: thesis:

end;

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

A5: n <> 0

proof

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

end;

then A7: 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 ) ) );
A8: Sum (sqr q) >= 0 by RVSUM_1:86;
A9: card (Seg n) = n by FINSEQ_1:57;
A10: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis:
assume A11: S₁[m] ; :: thesis:
set m1 = m + 1;
assume A12: (m + 1) + 1 <= n ; :: thesis:
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n), Xm being set such that
A13: card Xm = m and
A14: Xm c= Seg n and
A15: for k being Nat st k in Xm holds
(f . p) . k = q . k by A11, NAT_1:13;
set fp = f . p;
set sfp = sqr (f . p);
set sq = sqr q;
A16: m + 1 < n by A12, 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
A17: k in (Seg n) \ Xm and
A18: (sqr (f . p)) . k >= (sqr q) . k ;
A19: k in Seg n by A17, XBOOLE_0:def 5;
then A20: 1 <= k by FINSEQ_1:1;
set Xmk = Xm \/ {k};
A21: ( (sqr (f . p)) . k = ((f . p) . k) ^2 & (sqr q) . k = (q . k) ^2 ) by VALUED_1:11;
A22: {k} c= Seg n by A19, ZFMISC_1:31;
then A23: Xm \/ {k} c= Seg n by A14, XBOOLE_1:8;
A24: not k in Xm by A17, XBOOLE_0:def 5;
then card (Xm \/ {k}) = m + 1 by A13, A14, CARD_2:41;
then Xm \/ {k} c< Seg n by A9, A16, A23, XBOOLE_0:def 8;
then consider z being object such that
A25: z in Seg n and
A26: not z in Xm \/ {k} by XBOOLE_0:6;
reconsider z = z as Nat by A25;
A27: 1 <= z by A25, FINSEQ_1:1;
((f . p) . z) ^2 >= 0 by XREAL_1:63;
then A28: 0 + ((q . k) ^2) <= (((f . p) . z) ^2) + (((f . p) . k) ^2) by A18, A21, XREAL_1:7;
A29: z <= n by A25, FINSEQ_1:1;
A30: k <= n by A19, FINSEQ_1:1;
not z in {k} by A26, XBOOLE_0:def 3;
then A31: z <> k by TARSKI:def 1;

now :: thesis:

per cases by A31, XXREAL_0:1;

suppose A32: z < k ; :: thesis:

then consider r being Real such that
A33: ((Mx2Tran (Rotation (z,k,n,r))) . (f . p)) . k = q . k by A27, A28, A30, Th25;
( Mx2Tran (Rotation (z,k,n,r)) is {k,z} -support-yielding & Mx2Tran (Rotation (z,k,n,r)) is base_rotation ) by A27, A30, A32, Th28, Th26;
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 A33; :: thesis:

end;

suppose A34: z > k ; :: thesis:

then consider r being Real such that
A35: ((Mx2Tran (Rotation (k,z,n,r))) . (f . p)) . k = q . k by A20, A28, A29, Th24;
( Mx2Tran (Rotation (k,z,n,r)) is {z,k} -support-yielding & Mx2Tran (Rotation (k,z,n,r)) is base_rotation ) by A20, A29, A34, Th28, Th26;
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 A35; :: thesis:

end;

then consider g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A36: g is {k,z} -support-yielding and
A37: (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 A13, A14, A22, A24, CARD_2:41, XBOOLE_1:8; :: thesis:
let m be Nat; :: thesis:
A38: dom gf = the carrier of (TOP-REAL n) by FUNCT_2:52;
A39: dom g = the carrier of (TOP-REAL n) by FUNCT_2:52;
assume A40: m in Xm \/ {k} ; :: thesis:
then A41: ( m in Xm or m in {k} ) by XBOOLE_0:def 3;

per cases by A41, TARSKI:def 1;

suppose A42: m in Xm ; :: thesis:

then m <> k by A17, XBOOLE_0:def 5;
then not m in {k,z} by A26, A40, TARSKI:def 2;
then (g . (f . p)) . m = (f . p) . m by A36, A39;
hence (gf . p) . m = (f . p) . m by A38, FUNCT_1:12
.= q . m by A15, A42 ;
:: thesis:

end;

suppose m = k ; :: thesis:

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

end;

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

A44: Sum (sqr (f . p)) >= 0 by RVSUM_1:86;
( Sum (sqr q) >= 0 & |.p.| = |.(f . p).| ) by Def4, RVSUM_1:86;
then A45: Sum (sqr (f . p)) = Sum (sqr q) by A2, A44, SQUARE_1:28;
A46: len (sqr (f . p)) = len (f . p) by RVSUM_1:143;
A47: len (sqr q) = len q by RVSUM_1:143;
( 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 A46, A47, FINSEQ_2:92;
m < n by A16, NAT_1:13;
then Xm <> Seg n by A13, FINSEQ_1:57;
then Xm c< Seg n by A14, XBOOLE_0:def 8;
then consider z being object such that
A48: z in Seg n and
A49: not z in Xm by XBOOLE_0:6;
reconsider z = z as Nat by A48;
A50: z in (Seg n) \ Xm by A48, A49, 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 A51: k in Seg n ; :: thesis:

per cases by A51, XBOOLE_0:def 5;

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

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

end;

suppose k in Xm ; :: thesis:

then (f . p) . k = q . k by A15;
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 A45, A48, 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 A43, A50; :: thesis:

end;

reconsider n1 = n - 1 as Nat by A5;
A52: n1 + 1 = n ;
A53: 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 ) ; :: 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(A53, A10);
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n), X being set such that
A54: ( card X = n1 & X c= Seg n ) and
A55: for k being Nat st k in X holds
(f . p) . k = q . k by A52;
card ((Seg n) \ X) = n - n1 by A9, A54, CARD_2:44;
then consider z being object such that
A56: {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 A57: Sum (sqr q) = Sum (sqr (f . p)) by A2, A8, SQUARE_1:28;
A58: z in {z} by TARSKI:def 1;
then A59: z in Seg n by A56, XBOOLE_0:def 5;
reconsider z = z as Nat by A56, A58;
set fpz = (f . p) +* (z,(q . z));
A60: len (f . p) = n by CARD_1:def 7;
then A61: dom (f . p) = Seg n by FINSEQ_1:def 3;
A62: 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 A63: k in Seg n ;

per cases ;

suppose k = z ; :: thesis:

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

end;

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

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

end;

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

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

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

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

end;

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

1 < n by A1, A7, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider h being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) such that
A70: h is base_rotation and
A71: h . (f . p) = (f . p) +* (z,(- ((f . p) . z))) by A59, Th34;
dom (h * f) = the carrier of (TOP-REAL n) by FUNCT_2:52;
then (h * f) . p = (f . p) +* (z,(- ((f . p) . z))) by A71, FUNCT_1:12
.= q by A60, A62, A66, A69 ;
hence ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q ) by A70; :: thesis:

end;