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;

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

end;

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 )

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

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 )

( f2 is base_rotation & f2 * f1 is {n} -support-yielding )

then reconsider n1 = n - 1 as Nat ;

defpred S_{1}[ 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)

A9: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[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;defpred S

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

then reconsider S = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n1 ) } as Subset of (TOP-REAL n) ;
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;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

A9: for k being Nat st S

S

proof

A72:
S
let z be Nat; :: thesis: ( S_{1}[z] implies S_{1}[z + 1] )

assume A10: S_{1}[z]
; :: thesis: S_{1}[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

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 )

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

( 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;assume A10: S

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

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

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

z + 1 in { i where i is Element of NAT : ( z + 1 <= i & i <= n ) } /\ (Seg n)
by A22, A23, XBOOLE_0:def 4;
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

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

A35:
hg * f1 = h * (g * f1)
by RELAT_1:36;
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;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

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

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

take
hg
; :: thesis: (hg * f1) | S = id S
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;

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

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

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

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

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

set H = h . ((g * f1) . B);
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;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

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

A63:
for j being Nat st 1 <= j & j <= n holds
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;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

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

proof

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

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

end;

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

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

( 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

proof

for k being Nat holds S
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 = {}

(g * f1) | S = {} by A74;

hence (g * f1) | S = id S by A74; :: thesis: verum

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

take g = id (TOP-REAL n); :: thesis: (g * f1) | S = id S
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;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

(g * f1) | S = {} by A74;

hence (g * f1) | S = id S by A74; :: thesis: verum

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