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

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 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 (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q ) )

assume A2: |.p.| = |.q.| ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

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 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 (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q ) )

assume A2: |.p.| = |.q.| ; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

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

( f is base_rotation & f . p = q )

take I = id (TOP-REAL n); :: thesis: ( I is base_rotation & I . p = q )

thus ( I is base_rotation & I . p = q ) by A3; :: thesis: verum

end;thus ( I is base_rotation & I . p = q ) by A3; :: thesis: verum

suppose A4:
p <> q
; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

( f is base_rotation & f . p = q )

A5:
n <> 0

defpred S_{1}[ 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_{1}[m] holds

S_{1}[m + 1]

A52: n1 + 1 = n ;

A53: S_{1}[ 0 ]
_{1}[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

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;

end;proof

then A7:
n >= 1
by NAT_1:14;
assume A6:
n = 0
; :: thesis: contradiction

then p = 0. (TOP-REAL n) by EUCLID:77;

hence contradiction by A4, A6; :: thesis: verum

end;then p = 0. (TOP-REAL n) by EUCLID:77;

hence contradiction by A4, A6; :: thesis: verum

defpred S

( 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

S

proof

reconsider n1 = n - 1 as Nat by A5;
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A11: S_{1}[m]
; :: thesis: S_{1}[m + 1]

set m1 = m + 1;

assume A12: (m + 1) + 1 <= n ; :: thesis: 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 ) )

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;

end;assume A11: S

set m1 = m + 1;

assume A12: (m + 1) + 1 <= n ; :: thesis: 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 ) )

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

end;

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

( k in (Seg n) \ Xm & (sqr (f . p)) . k >= (sqr q) . k ) ; :: thesis: 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 ) )

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;

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 A13, A14, A22, A24, CARD_2:41, XBOOLE_1:8; :: 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 (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: (gf . p) . m = q . m

then A41: ( m in Xm or m in {k} ) by XBOOLE_0:def 3;

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

then consider g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that ( g is {k,z} -support-yielding & (g . (f . p)) . k = q . k )

per cases
( z < k or z > k )
by A31, XXREAL_0:1;

end;

suppose A32:
z < k
; :: thesis: 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 )

( 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 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: verum

end;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: verum

suppose A34:
z > k
; :: thesis: 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 )

( 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 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: verum

end;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: verum

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 A13, A14, A22, A24, CARD_2:41, XBOOLE_1:8; :: 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 (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: (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 A41, TARSKI:def 1;

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

(sqr (f . p)) . k < (sqr q) . k ; :: thesis: 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 ) )

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

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: verum

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

then
sfp . z >= sq . z
by A45, A48, RVSUM_1:83;
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

end;assume A51: k in Seg n ; :: thesis: sfp . k <= sq . k

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: verum

A52: n1 + 1 = n ;

A53: S

proof

for m being Nat holds S
assume
0 + 1 <= n
; :: thesis: ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) 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 (TOP-REAL n); :: 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;( card X = 0 & X c= Seg n & ( for k being Nat st k in X holds

(f . p) . k = q . k ) )

take f = id (TOP-REAL n); :: 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

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

A66:
( len ((f . p) +* (z,(q . z))) = len (f . p) & len q = n )
by CARD_1:def 7, FUNCT_7:97;
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 ;

end;assume ( 1 <= k & k <= n ) ; :: thesis: ((f . p) +* (z,(q . z))) . k = q . k

then A63: k in Seg n ;

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
( (f . p) . z = q . z or (f . p) . z = - (q . z) )
by A68, A57, SQUARE_1:40;

end;

suppose
(f . p) . z = q . z
; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

( f is base_rotation & f . p = q )

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: verum

end;hence ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q ) ; :: thesis: verum

suppose A69:
(f . p) . z = - (q . z)
; :: thesis: ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st

( f is base_rotation & f . p = q )

( f is base_rotation & f . p = q )

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: verum

end;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: verum