let n be Nat; :: thesis: for f1 being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation holds
ex f2 being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )
let f1 be homogeneous additive Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f1 is rotation implies ex f2 being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding ) )
set TR = TOP-REAL n;
assume A1: f1 is rotation ; :: thesis: ex f2 being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )
set cTR = the carrier of (TOP-REAL n);
set f = f1;
A2: dom f1 = the carrier of (TOP-REAL n) by FUNCT_2:52;
A3: rng f1 c= the carrier of (TOP-REAL n) by RELAT_1:def 19;

per cases ( n = 0 or n > 0 ) ;

suppose A4: n = 0 ; :: thesis: ex f2 being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )

take I = id (TOP-REAL n); :: thesis: ( I is base_rotation & I * f1 is {n} -support-yielding )
A5: dom (id the carrier of (TOP-REAL n)) = the carrier of (TOP-REAL n) by RELAT_1:45;
A6: for h being Function
for x being set st h in dom I & (I . h) . x <> h . x holds
x in {n} by A5, FUNCT_1:17;
A7: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by A4, JORDAN2C:105, EUCLID:22;
then ( rng (id the carrier of (TOP-REAL n)) = the carrier of (TOP-REAL n) & rng f1 = the carrier of (TOP-REAL n) ) by A3, RELAT_1:45, ZFMISC_1:33;
then f1 = id the carrier of (TOP-REAL n) by A2, A5, A7, FUNCT_1:7;
then I * f1 = I by A2, RELAT_1:52;
hence ( I is base_rotation & I * f1 is {n} -support-yielding ) by A6, Def1; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex f2 being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )

then reconsider n1 = n - 1 as Nat by NAT_1:20;
defpred S₁[ Nat] means ( $1 <= n - 1 implies for S being Subset of (TOP-REAL n) st S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= $1 ) } holds
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S );
set S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } ;
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } c= the carrier of (TOP-REAL n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } or x in the carrier of (TOP-REAL n) )
assume x in { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider j being Element of NAT such that
A8: x = Base_FinSeq (n,j) and
1 <= j and
j <= n1 ;
len (Base_FinSeq (n,j)) = n by MATRIXR2:74;
hence x in the carrier of (TOP-REAL n) by A8, TOPREAL7:17; :: thesis: verum

end;

then reconsider S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } as Subset of (TOP-REAL n) ;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let z be Nat; :: thesis: ( S₁[z] implies S₁[z + 1] )
assume A10: S₁[z] ; :: thesis: S₁[z + 1]
set z1 = z + 1;
set SS = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } ;
assume A11: z + 1 <= n - 1 ; :: thesis: for S being Subset of (TOP-REAL n) st S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z + 1 ) } holds
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S
then reconsider n1 = n - 1 as Element of NAT by INT_1:3;
A12: n1 < n1 + 1 by NAT_1:13;
then A13: z + 1 < n by A11, XXREAL_0:2;
set B = Base_FinSeq (n,(z + 1));
set X = { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } ;
let S be Subset of (TOP-REAL n); :: thesis: ( S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z + 1 ) } implies ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S )
assume A14: S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z + 1 ) } ; :: thesis: ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S
{ (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } c= S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } or x in S )
assume x in { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } ; :: thesis: x in S
then consider i being Element of NAT such that
A15: ( x = Base_FinSeq (n,i) & 1 <= i ) and
A16: i <= z ;
i < z + 1 by A16, NAT_1:13;
hence x in S by A14, A15; :: thesis: verum

end;

then reconsider SS = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= z ) } as Subset of (TOP-REAL n) by XBOOLE_1:1;
z < n1 by A11, NAT_1:13;
then consider g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A17: (g * f1) | SS = id SS by A10;
A18: n in NAT by ORDINAL1:def 12;
then A19: n in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } by A13;
n >= 1 by A12, NAT_1:14;
then n in Seg n by A18;
then A20: n in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) by A19, XBOOLE_0:def 4;
A21: card {(z + 1),n} = 2 by A11, A12, CARD_2:57;
A22: 1 <= z + 1 by NAT_1:11;
then A23: z + 1 in Seg n by A13;
Base_FinSeq (n,(z + 1)) in S by A14, A22;
then reconsider B = Base_FinSeq (n,(z + 1)) as Point of (TOP-REAL n) ;
set gfB = (g * f1) . B;
A24: z + 1 in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } by A13;
then consider h being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n) such that
A25: ( h is { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } -support-yielding & h is base_rotation ) and
A26: ( card ( { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)) > 1 implies (h . ((g * f1) . B)) . (z + 1) >= 0 ) and
A27: for i being Nat st i in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) & i <> z + 1 holds
(h . ((g * f1) . B)) . i = 0 by A23, Th29;
reconsider hg = h * g as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A25;
A28: dom (hg * f1) = the carrier of (TOP-REAL n) by FUNCT_2:52;
A29: for x being set st x in SS holds
( ((h * g) * f1) . x = x & h . x = x )

proof

let x be set ; :: thesis: ( x in SS implies ( ((h * g) * f1) . x = x & h . x = x ) )
assume A30: x in SS ; :: thesis: ( ((h * g) * f1) . x = x & h . x = x )
reconsider B = x as Point of (TOP-REAL n) by A30;
((g * f1) | SS) . x = (g * f1) . x by A30, FUNCT_1:49;
then A31: (g * f1) . x = x by A17, A30, FUNCT_1:17;
A32: ex i being Element of NAT st
( x = Base_FinSeq (n,i) & 1 <= i & i <= z ) by A30;
A33: for j being Nat st j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) holds
B . j = 0

proof

let j be Nat; :: thesis: ( j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) implies B . j = 0 )
assume A34: j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) ; :: thesis: B . j = 0
then j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } by XBOOLE_0:def 4;
then ex I being Element of NAT st
( I = j & z + 1 <= I & I <= n ) ;
then A35: z < j by NAT_1:13;
j in Seg n by A34, XBOOLE_0:def 4;
then ( 1 <= j & j <= n ) by FINSEQ_1:1;
hence B . j = 0 by A32, A35, MATRIXR2:76; :: thesis: verum

end;

A36: hg * f1 = h * (g * f1) by RELAT_1:36;
then (h * (g * f1)) . x = h . ((g * f1) . x) by A28, A30, FUNCT_1:12;
hence ( ((h * g) * f1) . x = x & h . x = x ) by A25, A31, A33, A36, Th32; :: thesis: verum

end;

z + 1 in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) by A23, A24, XBOOLE_0:def 4;
then {(z + 1),n} c= { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) by A20, ZFMISC_1:32;
then A37: 1 + 1 <= card ( { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)) by A21, NAT_1:43;
A38: for x being set st x in S holds
((hg * f1) | S) . x = (id S) . x

proof

let x be set ; :: thesis: ( x in S implies ((hg * f1) | S) . x = (id S) . x )
assume A39: x in S ; :: thesis: ((hg * f1) | S) . x = (id S) . x
A40: (id S) . x = x by A39, FUNCT_1:17;
A41: hg * f1 = h * (g * f1) by RELAT_1:36;
A42: ((hg * f1) | S) . x = (hg * f1) . x by A39, FUNCT_1:49;
consider i being Element of NAT such that
A43: x = Base_FinSeq (n,i) and
A44: 1 <= i and
A45: i <= z + 1 by A14, A39;

per cases ( i <= z or i = z + 1 ) by A45, NAT_1:8;

suppose i <= z ; :: thesis: ((hg * f1) | S) . x = (id S) . x

then x in SS by A43, A44;
hence ((hg * f1) | S) . x = (id S) . x by A29, A40, A42; :: thesis: verum

end;

suppose A46: i = z + 1 ; :: thesis: ((hg * f1) | S) . x = (id S) . x

set H = h . ((g * f1) . B);
A47: (h * (g * f1)) . x = h . ((g * f1) . B) by A28, A41, A43, A46, FUNCT_1:12;
A48: len (h . ((g * f1) . B)) = n by CARD_1:def 7;
A49: for j being Nat st j in Seg n & j < z + 1 holds
(h . ((g * f1) . B)) . j = 0

proof

let j be Nat; :: thesis: ( j in Seg n & j < z + 1 implies (h . ((g * f1) . B)) . j = 0 )
assume that
A50: j in Seg n and
A51: j < z + 1 ; :: thesis: (h . ((g * f1) . B)) . j = 0
A52: 1 <= j by A50, FINSEQ_1:1;
j <= z by A51, NAT_1:13;
then A53: Base_FinSeq (n,j) in SS by A50, A52;
then reconsider Bnj = Base_FinSeq (n,j) as Point of (TOP-REAL n) ;
((h * g) * f1) . Bnj = Bnj by A29, A53;
then A54: Bnj + (h . ((g * f1) . B)) = ((h * g) * f1) . (Bnj + B) by A41, A43, A46, A47, GRCAT_1:def 8;
A55: len Bnj = n by CARD_1:def 7;
|.(((h * g) * f1) . (Bnj + B)).| = |.(Bnj + B).| by A1, A25, Def4;
then A56: |.(Bnj + B).| ^2 = ((|.Bnj.| ^2) + (2 * |((h . ((g * f1) . B)),Bnj)|)) + (|.(h . ((g * f1) . B)).| ^2) by A48, A54, A55, EUCLID_2:11;
A57: Bnj = (0* n) +* (j,1) by MATRIXR2:def 4;
len B = n by CARD_1:def 7;
then A58: |.(Bnj + B).| ^2 = ((|.Bnj.| ^2) + (2 * |(B,Bnj)|)) + (|.B.| ^2) by A55, EUCLID_2:11;
A59: j <= n by A50, FINSEQ_1:1;
|.(h . ((g * f1) . B)).| = |.B.| by A1, A25, A43, A46, A47, Def4;
then (B . j) * 1 = |((h . ((g * f1) . B)),Bnj)| by A56, A57, A58, TOPREALC:16
.= ((h . ((g * f1) . B)) . j) * 1 by A57, TOPREALC:16 ;
hence (h . ((g * f1) . B)) . j = 0 by A51, A52, A59, MATRIXR2:76; :: thesis: verum

end;

set H = h . ((g * f1) . B);
set 0H = (0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)));
A60: len (0* n) = n by CARD_1:def 7;
A61: for j being Nat st j in Seg n & j > z + 1 holds
(h . ((g * f1) . B)) . j = 0

proof

let j be Nat; :: thesis: ( j in Seg n & j > z + 1 implies (h . ((g * f1) . B)) . j = 0 )
assume that
A62: j in Seg n and
A63: j > z + 1 ; :: thesis: (h . ((g * f1) . B)) . j = 0
j <= n by A62, FINSEQ_1:1;
then j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } by A62, A63;
then j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) by A62, XBOOLE_0:def 4;
hence (h . ((g * f1) . B)) . j = 0 by A27, A63; :: thesis: verum

end;

A64: for j being Nat st 1 <= j & j <= n holds
(h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j )
assume ( 1 <= j & j <= n ) ; :: thesis: (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j
then A65: j in Seg n by FINSEQ_1:1;
then A66: j in dom (0* n) by A60, FINSEQ_1:def 3;

per cases ( j = z + 1 or j <> z + 1 ) ;

suppose j = z + 1 ; :: thesis: (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j

hence (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j by A66, FUNCT_7:31; :: thesis: verum

end;

suppose A67: j <> z + 1 ; :: thesis: (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j

then ( j > z + 1 or j < z + 1 ) by XXREAL_0:1;
then A68: (h . ((g * f1) . B)) . j = 0 by A49, A61, A65;
((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j = (0* n) . j by A67, FUNCT_7:32;
hence (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j by A65, A68, FINSEQ_2:57; :: thesis: verum

end;

end;

end;

( len (h . ((g * f1) . B)) = n & len ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) = len (0* n) ) by CARD_1:def 7, FUNCT_7:97;
then A69: (0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1))) = h . ((g * f1) . B) by A60, A64, FINSEQ_1:14;
A70: |.((g * f1) . B).| = |.B.| by A1, Def4;
A71: B = (0* n) +* ((z + 1),1) by MATRIXR2:def 4;
then A72: |.B.| = abs 1 by A23, TOPREALC:13
.= 1 by ABSVALUE:def 1 ;
( |.(h . ((g * f1) . B)).| = |.((g * f1) . B).| & abs ((h . ((g * f1) . B)) . (z + 1)) = (h . ((g * f1) . B)) . (z + 1) ) by A25, A26, A37, Def4, ABSVALUE:def 1, NAT_1:13;
then h . ((g * f1) . B) = B by A23, A69, A71, A72, A70, TOPREALC:13;
hence ((hg * f1) | S) . x = (id S) . x by A39, A40, A41, A43, A46, A47, FUNCT_1:49; :: thesis: verum

end;

end;

end;

take hg ; :: thesis: (hg * f1) | S = id S
( dom (id S) = S & dom ((hg * f1) | S) = S ) by A28, RELAT_1:45, RELAT_1:62;
hence (hg * f1) | S = id S by A38, FUNCT_1:2; :: thesis: verum

end;

A73: S₁[ 0 ]

proof

assume 0 <= n - 1 ; :: thesis: for S being Subset of (TOP-REAL n) st S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= 0 ) } holds
ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S
let S be Subset of (TOP-REAL n); :: thesis: ( S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= 0 ) } implies ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S )
assume A74: S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= 0 ) } ; :: thesis: ex g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st (g * f1) | S = id S
A75: S = {}

proof

assume S <> {} ; :: thesis: contradiction
then consider x being set such that
A76: x in S by XBOOLE_0:def 1;
ex i being Element of NAT st
( x = Base_FinSeq (n,i) & 1 <= i & i <= 0 ) by A74, A76;
hence contradiction ; :: thesis: verum

end;

take g = id (TOP-REAL n); :: thesis: (g * f1) | S = id S
(g * f1) | S = {} by A75;
hence (g * f1) | S = id S by A75; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A73, A9);
then consider g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A77: (g * f1) | S = id S ;
take g ; :: thesis: ( g is base_rotation & g * f1 is {n} -support-yielding )
set gf = g * f1;
thus g is base_rotation ; :: thesis: g * f1 is {n} -support-yielding
let p be Function; :: according to MATRTOP3:def 1 :: thesis: for x being set st p in dom (g * f1) & ((g * f1) . p) . x <> p . x holds
x in {n}
let x be set ; :: thesis: ( p in dom (g * f1) & ((g * f1) . p) . x <> p . x implies x in {n} )
assume that
A78: p in dom (g * f1) and
A79: ((g * f1) . p) . x <> p . x ; :: thesis: x in {n}
reconsider p = p as Point of (TOP-REAL n) by A78, FUNCT_2:52;
len ((g * f1) . p) = n by CARD_1:def 7;
then dom ((g * f1) . p) = Seg n by FINSEQ_1:def 3;
then A80: ( not x in Seg n implies ((g * f1) . p) . x = {} ) by FUNCT_1:def 2;
len p = n by CARD_1:def 7;
then dom p = Seg n by FINSEQ_1:def 3;
then A81: x in Seg n by A79, A80, FUNCT_1:def 2;
assume A82: not x in {n} ; :: thesis: contradiction
reconsider x = x as Nat by A81;
A83: x <= n by A81, FINSEQ_1:1;
x <> n by A82, TARSKI:def 1;
then x < n1 + 1 by A83, XXREAL_0:1;
then A84: x <= n1 by NAT_1:13;
( x in NAT & 1 <= x ) by A81, FINSEQ_1:1;
then Base_FinSeq (n,x) in S by A84;
then Base_FinSeq (n,x) in Lin S by RLVECT_3:15;
then ((g * f1) . p) . x = p . x by A1, A77, A81, Th31;
hence contradiction by A79; :: thesis: verum

end;

end;