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 base_rotation & f . p = q )

let p, q be Point of (); :: thesis: ( n <> 1 & |.p.| = |.q.| implies ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q ) )

set TR = TOP-REAL n;
assume A1: n <> 1 ; :: thesis: ( not |.p.| = |.q.| or ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q ) )

assume A2: |.p.| = |.q.| ; :: thesis: ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q )

per cases ( p = q or p <> q ) ;
suppose A3: p = q ; :: thesis: ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q )

take I = id (); :: thesis: ( I is base_rotation & I . p = q )
thus ( I is base_rotation & I . p = q ) by A3; :: thesis: verum
end;
suppose A4: p <> q ; :: thesis: ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q )

A5: n <> 0
proof
assume A6: n = 0 ; :: thesis: contradiction
then p = 0. () by EUCLID:77;
hence contradiction by A4, A6; :: thesis: verum
end;
then A7: n >= 1 by NAT_1:14;
defpred S1[ Nat] means ( \$1 + 1 <= n implies ex f being base_rotation Function of (),() 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 S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A11: S1[m] ; :: thesis: S1[m + 1]
set m1 = m + 1;
assume A12: (m + 1) + 1 <= n ; :: thesis: ex f being base_rotation Function of (),() 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 ) )

then consider f being base_rotation Function of (),(), 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 ;
set fp = f . p;
set sfp = sqr (f . p);
set sq = sqr q;
A16: m + 1 < n by ;
per cases ( ex k being Nat st
( k in (Seg n) \ Xm & (sqr (f . p)) . k >= (sqr q) . k ) or for k being Nat st k in (Seg n) \ Xm holds
(sqr (f . p)) . k < (sqr q) . k )
;
suppose ex k being Nat st
( k in (Seg n) \ Xm & (sqr (f . p)) . k >= (sqr q) . k ) ; :: thesis: ex f being base_rotation Function of (),() 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 ) )

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 ;
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 ;
then A23: Xm \/ {k} c= Seg n by ;
A24: not k in Xm by ;
then card (Xm \/ {k}) = m + 1 by ;
then Xm \/ {k} c< Seg n by ;
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 ;
((f . p) . z) ^2 >= 0 by XREAL_1:63;
then A28: 0 + ((q . k) ^2) <= (((f . p) . z) ^2) + (((f . p) . k) ^2) by ;
A29: z <= n by ;
A30: k <= n by ;
not z in {k} by ;
then A31: z <> k by TARSKI:def 1;
now :: thesis: ex g being base_rotation Function of (),() st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )
per cases ( z < k or z > k ) by ;
suppose A32: z < k ; :: thesis: ex g being base_rotation Function of (),() st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )

then consider r being Real such that
A33: ((Mx2Tran (Rotation (z,k,n,r))) . (f . p)) . k = q . k by ;
( Mx2Tran (Rotation (z,k,n,r)) is {k,z} -support-yielding & Mx2Tran (Rotation (z,k,n,r)) is base_rotation ) by ;
hence ex g being base_rotation Function of (),() st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k ) by A33; :: thesis: verum
end;
suppose A34: z > k ; :: thesis: ex g being base_rotation Function of (),() st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )

then consider r being Real such that
A35: ((Mx2Tran (Rotation (k,z,n,r))) . (f . p)) . k = q . k by ;
( Mx2Tran (Rotation (k,z,n,r)) is {z,k} -support-yielding & Mx2Tran (Rotation (k,z,n,r)) is base_rotation ) by ;
hence ex g being base_rotation Function of (),() st
( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k ) by A35; :: thesis: verum
end;
end;
end;
then consider g being base_rotation Function of (),() such that
A36: g is {k,z} -support-yielding and
A37: (g . (f . p)) . k = q . k ;
take gf = g * f; :: thesis: ex X being set st
( card X = m + 1 & X c= Seg n & ( for k being Nat st k in X holds
(gf . p) . k = q . k ) )

take Xm \/ {k} ; :: thesis: ( card (Xm \/ {k}) = m + 1 & Xm \/ {k} c= Seg n & ( for k being Nat st k in Xm \/ {k} holds
(gf . p) . k = q . k ) )

thus ( card (Xm \/ {k}) = m + 1 & Xm \/ {k} c= Seg n ) by ; :: thesis: for k being Nat st k in Xm \/ {k} holds
(gf . p) . k = q . k

let m be Nat; :: thesis: ( m in Xm \/ {k} implies (gf . p) . m = q . m )
A38: dom gf = the carrier of () by FUNCT_2:52;
A39: dom g = the carrier of () by FUNCT_2:52;
assume A40: m in Xm \/ {k} ; :: thesis: (gf . p) . m = q . m
then A41: ( m in Xm or m in {k} ) by XBOOLE_0:def 3;
per cases ( m in Xm or m = k ) by ;
suppose A42: m in Xm ; :: thesis: (gf . p) . m = q . m
then m <> k by ;
then not m in {k,z} by ;
then (g . (f . p)) . m = (f . p) . m by ;
hence (gf . p) . m = (f . p) . m by
.= q . m by ;
:: thesis: verum
end;
suppose m = k ; :: thesis: (gf . p) . m = q . m
hence (gf . p) . m = q . m by ; :: thesis: verum
end;
end;
end;
suppose A43: for k being Nat st k in (Seg n) \ Xm holds
(sqr (f . p)) . k < (sqr q) . k ; :: thesis: ex f being base_rotation Function of (),() 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 ) )

A44: Sum (sqr (f . p)) >= 0 by RVSUM_1:86;
( Sum (sqr q) >= 0 & |.p.| = |.(f . p).| ) by ;
then A45: Sum (sqr (f . p)) = Sum (sqr q) by ;
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 ;
m < n by ;
then Xm <> Seg n by ;
then Xm c< Seg n by ;
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 ;
for k being Nat st k in Seg n holds
sfp . k <= sq . k
proof
let k be Nat; :: thesis: ( k in Seg n implies sfp . k <= sq . k )
assume A51: k in Seg n ; :: thesis: sfp . k <= sq . k
per cases ( k in (Seg n) \ Xm or k in Xm ) by ;
suppose k in (Seg n) \ Xm ; :: thesis: sfp . k <= sq . k
hence sfp . k <= sq . k by A43; :: thesis: verum
end;
suppose k in Xm ; :: thesis: sfp . k <= sq . k
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: verum
end;
end;
end;
then sfp . z >= sq . z by ;
hence ex f being base_rotation Function of (),() 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 ; :: thesis: verum
end;
end;
end;
reconsider n1 = n - 1 as Nat by A5;
A52: n1 + 1 = n ;
A53: S1[ 0 ]
proof
assume 0 + 1 <= n ; :: thesis: ex f being base_rotation Function of (),() ex X being set st
( card X = 0 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) )

take f = id (); :: thesis: ex X being set st
( card X = 0 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) )

take X = {} ; :: thesis: ( card X = 0 & X c= Seg n & ( for k being Nat st k in X holds
(f . p) . k = q . k ) )

thus ( card X = 0 & X c= Seg n ) ; :: thesis: for k being Nat st k in X holds
(f . p) . k = q . k

let k be Nat; :: thesis: ( k in X implies (f . p) . k = q . k )
assume k in X ; :: thesis: (f . p) . k = q . k
hence (f . p) . k = q . k ; :: thesis: verum
end;
for m being Nat holds S1[m] from then consider f being base_rotation Function of (),(), 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 ;
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 ;
then A57: Sum (sqr q) = Sum (sqr (f . p)) by ;
A58: z in {z} by TARSKI:def 1;
then A59: z in Seg n by ;
reconsider z = z as Nat by ;
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: ( 1 <= k & k <= n implies ((f . p) +* (z,(q . z))) . k = q . k )
assume ( 1 <= k & k <= n ) ; :: thesis: ((f . p) +* (z,(q . z))) . k = q . k
then A63: k in Seg n ;
per cases ( k = z or k <> z ) ;
suppose k = z ; :: thesis: ((f . p) +* (z,(q . z))) . k = q . k
hence ((f . p) +* (z,(q . z))) . k = q . k by ; :: thesis: verum
end;
suppose A64: k <> z ; :: thesis: ((f . p) +* (z,(q . z))) . k = q . k
then not k in (Seg n) \ X by ;
then A65: k in X by ;
((f . p) +* (z,(q . z))) . k = (f . p) . k by ;
hence ((f . p) +* (z,(q . z))) . k = q . k by ; :: thesis: verum
end;
end;
end;
A66: ( len ((f . p) +* (z,(q . z))) = len (f . p) & len q = n ) by ;
then A67: (f . p) +* (z,(q . z)) = q by ;
then A68: Sum (sqr q) = ((Sum (sqr (f . p))) - (((f . p) . z) ^2)) + ((q . z) ^2) by ;
per cases ) . z = q . z or (f . p) . z = - (q . z) ) by ;
suppose (f . p) . z = q . z ; :: thesis: ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q )

then f . p = q by ;
hence ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q ) ; :: thesis: verum
end;
suppose A69: (f . p) . z = - (q . z) ; :: thesis: ex f being additive homogeneous Function of (),() st
( f is base_rotation & f . p = q )

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