let n be Nat; :: thesis: for f1 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation holds
ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f2 is base_rotation & f2 * f1 is {n} -support-yielding )
let f1 be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f1 is rotation implies ex f2 being additive homogeneous 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 additive homogeneous 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 additive homogeneous 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) ;
A6: for h being Function
for x being set st h in dom I & (I . h) . x <> h . x holds
x in {n} by FUNCT_1:17;
A7: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by A4, EUCLID:22, EUCLID:77;
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, 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; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex f2 being additive homogeneous 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 ;
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 object ; :: 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, TOPREAL3:46; :: 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 object ; :: 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;
n in NAT by ORDINAL1:def 12;
then A18: 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 ;
then A19: n in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) by A18, XBOOLE_0:def 4;
A20: card {(z + 1),n} = 2 by A11, A12, CARD_2:57;
A21: 1 <= z + 1 by NAT_1:11;
then A22: z + 1 in Seg n by A13;
Base_FinSeq (n,(z + 1)) in S by A14, A21;
then reconsider B = Base_FinSeq (n,(z + 1)) as Point of (TOP-REAL n) ;
set gfB = (g * f1) . B;
A23: z + 1 in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } by A13;
then consider h being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) such that
A24: ( h is { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } -support-yielding & h is base_rotation ) and
A25: ( 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
A26: 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 A22, Th30;
reconsider hg = h * g as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A24;
A27: dom (hg * f1) = the carrier of (TOP-REAL n) by FUNCT_2:52;
A28: 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 A29: x in SS ; :: thesis: ( ((h * g) * f1) . x = x & h . x = x )
reconsider B = x as Point of (TOP-REAL n) by A29;
((g * f1) | SS) . x = (g * f1) . x by A29, FUNCT_1:49;
then A30: (g * f1) . x = x by A17, A29, FUNCT_1:17;
A31: ex i being Element of NAT st
( x = Base_FinSeq (n,i) & 1 <= i & i <= z ) by A29;
A32: 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 A33: 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 A34: z < j by NAT_1:13;
j in Seg n by A33, XBOOLE_0:def 4;
then ( 1 <= j & j <= n ) by FINSEQ_1:1;
hence B . j = 0 by A31, A34, MATRIXR2:76; :: thesis: verum

end;

A35: hg * f1 = h * (g * f1) by RELAT_1:36;
then (h * (g * f1)) . x = h . ((g * f1) . x) by A27, A29, FUNCT_1:12;
hence ( ((h * g) * f1) . x = x & h . x = x ) by A24, A30, A32, A35, Th33; :: thesis: verum

end;

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

proof

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

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

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

then x in SS by A42, A43;
hence ((hg * f1) | S) . x = (id S) . x by A28, A39, A41; :: thesis: verum

end;

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

set H = h . ((g * f1) . B);
A46: (h * (g * f1)) . x = h . ((g * f1) . B) by A27, A40, A42, A45, FUNCT_1:12;
A47: len (h . ((g * f1) . B)) = n by CARD_1:def 7;
A48: 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
A49: j in Seg n and
A50: j < z + 1 ; :: thesis: (h . ((g * f1) . B)) . j = 0
A51: 1 <= j by A49, FINSEQ_1:1;
j <= z by A50, NAT_1:13;
then A52: Base_FinSeq (n,j) in SS by A49, A51;
then reconsider Bnj = Base_FinSeq (n,j) as Point of (TOP-REAL n) ;
((h * g) * f1) . Bnj = Bnj by A28, A52;
then A53: Bnj + (h . ((g * f1) . B)) = ((h * g) * f1) . (Bnj + B) by A40, A42, A45, A46, VECTSP_1:def 20;
A54: len Bnj = n by CARD_1:def 7;
|.(((h * g) * f1) . (Bnj + B)).| = |.(Bnj + B).| by A1, A24, Def4;
then A55: |.(Bnj + B).| ^2 = ((|.Bnj.| ^2) + (2 * |((h . ((g * f1) . B)),Bnj)|)) + (|.(h . ((g * f1) . B)).| ^2) by A47, A53, A54, EUCLID_2:11;
A56: Bnj = (0* n) +* (j,1) by MATRIXR2:def 4;
len B = n by CARD_1:def 7;
then A57: |.(Bnj + B).| ^2 = ((|.Bnj.| ^2) + (2 * |(B,Bnj)|)) + (|.B.| ^2) by A54, EUCLID_2:11;
A58: j <= n by A49, FINSEQ_1:1;
|.(h . ((g * f1) . B)).| = |.B.| by A1, A24, A42, A45, A46, Def4;
then (B . j) * 1 = |((h . ((g * f1) . B)),Bnj)| by A55, A56, A57, TOPREALC:16
.= ((h . ((g * f1) . B)) . j) * 1 by A56, TOPREALC:16 ;
hence (h . ((g * f1) . B)) . j = 0 by A50, A51, A58, MATRIXR2:76; :: thesis: verum

end;

set H = h . ((g * f1) . B);
set 0H = (0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)));
A59: len (0* n) = n by CARD_1:def 7;
A60: 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
A61: j in Seg n and
A62: j > z + 1 ; :: thesis: (h . ((g * f1) . B)) . j = 0
j <= n by A61, FINSEQ_1:1;
then j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } by A61, A62;
then j in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n) by A61, XBOOLE_0:def 4;
hence (h . ((g * f1) . B)) . j = 0 by A26, A62; :: thesis: verum

end;

A63: 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 A64: j in Seg n ;
then A65: j in dom (0* n) by A59, 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 A65, FUNCT_7:31; :: thesis: verum

end;

suppose A66: 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 A67: (h . ((g * f1) . B)) . j = 0 by A48, A60, A64;
((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j = (0* n) . j by A66, FUNCT_7:32;
hence (h . ((g * f1) . B)) . j = ((0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1)))) . j by A67; :: 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 A68: (0* n) +* ((z + 1),((h . ((g * f1) . B)) . (z + 1))) = h . ((g * f1) . B) by A59, A63;
A69: |.((g * f1) . B).| = |.B.| by A1, Def4;
A70: B = (0* n) +* ((z + 1),1) by MATRIXR2:def 4;
then A71: |.B.| = |.1.| by A22, TOPREALC:13
.= 1 by ABSVALUE:def 1 ;
( |.(h . ((g * f1) . B)).| = |.((g * f1) . B).| & |.((h . ((g * f1) . B)) . (z + 1)).| = (h . ((g * f1) . B)) . (z + 1) ) by A24, A25, A36, Def4, ABSVALUE:def 1, NAT_1:13;
then h . ((g * f1) . B) = B by A22, A68, A70, A71, A69, TOPREALC:13;
hence ((hg * f1) | S) . x = (id S) . x by A38, A39, A40, A42, A45, A46, 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 A27, RELAT_1:62;
hence (hg * f1) | S = id S by A37, FUNCT_1:2; :: thesis: verum

end;

A72: 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 A73: 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
A74: S = {}

proof

assume S <> {} ; :: thesis: contradiction
then consider x being object such that
A75: 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 A73, A75;
hence contradiction ; :: thesis: verum

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A72, A9);
then consider g being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A76: (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
A77: p in dom (g * f1) and
A78: ((g * f1) . p) . x <> p . x ; :: thesis: x in {n}
reconsider p = p as Point of (TOP-REAL n) by A77, 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 A79: ( 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 A80: x in Seg n by A78, A79, FUNCT_1:def 2;
assume A81: not x in {n} ; :: thesis: contradiction
reconsider x = x as Nat by A80;
A82: x <= n by A80, FINSEQ_1:1;
x <> n by A81, TARSKI:def 1;
then x < n1 + 1 by A82, XXREAL_0:1;
then A83: x <= n1 by NAT_1:13;
( x in NAT & 1 <= x ) by A80, FINSEQ_1:1;
then Base_FinSeq (n,x) in S by A83;
then Base_FinSeq (n,x) in Lin S by RLVECT_3:15;
then ((g * f1) . p) . x = p . x by A1, A76, A80, Th32;
hence contradiction by A78; :: thesis: verum

end;

end;