set TR = TOP-REAL n;

set G = GFuncs the carrier of (TOP-REAL n);

defpred S_{1}[ Nat] means for F being FinSequence of (GFuncs the carrier of (TOP-REAL n))

for f being Function of (TOP-REAL n),(TOP-REAL n) st len F = n & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) holds

f " is base_rotation ;

consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that

A1: ( f = Product F & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) by Def5;

A2: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
_{1}[i]
from NAT_1:sch 2(A19, A2);

then S_{1}[ len F]
;

hence f " is base_rotation by A1; :: thesis: verum

set G = GFuncs the carrier of (TOP-REAL n);

defpred S

for f being Function of (TOP-REAL n),(TOP-REAL n) st len F = n & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) holds

f " is base_rotation ;

consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that

A1: ( f = Product F & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) by Def5;

A2: for i being Nat st S

S

proof

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

assume A3: S_{1}[z]
; :: thesis: S_{1}[z + 1]

set z1 = z + 1;

let F be FinSequence of (GFuncs the carrier of (TOP-REAL n)); :: thesis: for f being Function of (TOP-REAL n),(TOP-REAL n) st len F = z + 1 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) holds

f " is base_rotation

let f be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( len F = z + 1 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) implies f " is base_rotation )

assume that

A4: len F = z + 1 and

A5: Product F = f and

A6: for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ; :: thesis: f " is base_rotation

set Fz = F | z;

reconsider fz = Product (F | z) as Function of (TOP-REAL n),(TOP-REAL n) by MONOID_0:73;

1 <= z + 1 by NAT_1:11;

then z + 1 in dom F by A4, FINSEQ_3:25;

then consider i, j being Nat, r being Real such that

A7: ( 1 <= i & i < j & j <= n ) and

A8: F . (z + 1) = Mx2Tran (Rotation (i,j,n,r)) by A6;

set m = Mx2Tran (Rotation (i,j,n,r));

reconsider M = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of (TOP-REAL n)) by MONOID_0:73;

F = (F | z) ^ <*M*> by A4, A8, FINSEQ_3:55;

then A9: f = (Product (F | z)) * M by A5, GROUP_4:6

.= (Mx2Tran (Rotation (i,j,n,r))) * fz by MONOID_0:70 ;

A10: dom (F | z) c= dom F by RELAT_1:60;

( Det (Rotation (i,j,n,r)) <> 0. F_Real & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) ) by A7, Lm5, Th13;

then A14: (Mx2Tran (Rotation (i,j,n,r))) " = Mx2Tran (Rotation (i,j,n,(- r))) by MATRTOP1:43;

A15: ( rng (Mx2Tran (Rotation (i,j,n,r))) = [#] (TOP-REAL n) & Mx2Tran (Rotation (i,j,n,r)) is one-to-one & dom (Mx2Tran (Rotation (i,j,n,r))) = [#] (TOP-REAL n) ) by TOPS_2:def 5;

then Mx2Tran (Rotation (i,j,n,r)) is onto by FUNCT_2:def 3;

then A16: (Mx2Tran (Rotation (i,j,n,r))) " = (Mx2Tran (Rotation (i,j,n,r))) " by A15, TOPS_2:def 4;

len (F | z) = z by A4, FINSEQ_1:59, NAT_1:11;

then A17: fz " is base_rotation by A3, A11;

( fz is one-to-one & dom fz = [#] (TOP-REAL n) & rng fz = [#] (TOP-REAL n) ) by A13, TOPS_2:def 5;

then A18: f " = (fz ") * ((Mx2Tran (Rotation (i,j,n,r))) ") by A9, A15, TOPS_2:53;

Mx2Tran (Rotation (i,j,n,(- r))) is base_rotation by A7, Th28;

hence f " is base_rotation by A14, A16, A17, A18; :: thesis: verum

end;assume A3: S

set z1 = z + 1;

let F be FinSequence of (GFuncs the carrier of (TOP-REAL n)); :: thesis: for f being Function of (TOP-REAL n),(TOP-REAL n) st len F = z + 1 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) holds

f " is base_rotation

let f be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( len F = z + 1 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) implies f " is base_rotation )

assume that

A4: len F = z + 1 and

A5: Product F = f and

A6: for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ; :: thesis: f " is base_rotation

set Fz = F | z;

reconsider fz = Product (F | z) as Function of (TOP-REAL n),(TOP-REAL n) by MONOID_0:73;

1 <= z + 1 by NAT_1:11;

then z + 1 in dom F by A4, FINSEQ_3:25;

then consider i, j being Nat, r being Real such that

A7: ( 1 <= i & i < j & j <= n ) and

A8: F . (z + 1) = Mx2Tran (Rotation (i,j,n,r)) by A6;

set m = Mx2Tran (Rotation (i,j,n,r));

reconsider M = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of (TOP-REAL n)) by MONOID_0:73;

F = (F | z) ^ <*M*> by A4, A8, FINSEQ_3:55;

then A9: f = (Product (F | z)) * M by A5, GROUP_4:6

.= (Mx2Tran (Rotation (i,j,n,r))) * fz by MONOID_0:70 ;

A10: dom (F | z) c= dom F by RELAT_1:60;

A11: now :: thesis: for k being Nat st k in dom (F | z) holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) )

then A13:
fz is base_rotation
;ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) )

let k be Nat; :: thesis: ( k in dom (F | z) implies ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) ) )

assume A12: k in dom (F | z) ; :: thesis: ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) )

then (F | z) . k = F . k by FUNCT_1:47;

hence ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) ) by A6, A10, A12; :: thesis: verum

end;( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) ) )

assume A12: k in dom (F | z) ; :: thesis: ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) )

then (F | z) . k = F . k by FUNCT_1:47;

hence ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & (F | z) . k = Mx2Tran (Rotation (i,j,n,r)) ) by A6, A10, A12; :: thesis: verum

( Det (Rotation (i,j,n,r)) <> 0. F_Real & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) ) by A7, Lm5, Th13;

then A14: (Mx2Tran (Rotation (i,j,n,r))) " = Mx2Tran (Rotation (i,j,n,(- r))) by MATRTOP1:43;

A15: ( rng (Mx2Tran (Rotation (i,j,n,r))) = [#] (TOP-REAL n) & Mx2Tran (Rotation (i,j,n,r)) is one-to-one & dom (Mx2Tran (Rotation (i,j,n,r))) = [#] (TOP-REAL n) ) by TOPS_2:def 5;

then Mx2Tran (Rotation (i,j,n,r)) is onto by FUNCT_2:def 3;

then A16: (Mx2Tran (Rotation (i,j,n,r))) " = (Mx2Tran (Rotation (i,j,n,r))) " by A15, TOPS_2:def 4;

len (F | z) = z by A4, FINSEQ_1:59, NAT_1:11;

then A17: fz " is base_rotation by A3, A11;

( fz is one-to-one & dom fz = [#] (TOP-REAL n) & rng fz = [#] (TOP-REAL n) ) by A13, TOPS_2:def 5;

then A18: f " = (fz ") * ((Mx2Tran (Rotation (i,j,n,r))) ") by A9, A15, TOPS_2:53;

Mx2Tran (Rotation (i,j,n,(- r))) is base_rotation by A7, Th28;

hence f " is base_rotation by A14, A16, A17, A18; :: thesis: verum

proof

for i being Nat holds S
let F be FinSequence of (GFuncs the carrier of (TOP-REAL n)); :: thesis: for f being Function of (TOP-REAL n),(TOP-REAL n) st len F = 0 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) holds

f " is base_rotation

let f be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( len F = 0 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) implies f " is base_rotation )

assume that

A20: len F = 0 and

A21: Product F = f ; :: thesis: ( ex k being Nat st

( k in dom F & ( for i, j being Nat

for r being Real holds

( not 1 <= i or not i < j or not j <= n or not F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) or f " is base_rotation )

F = <*> the carrier of (GFuncs the carrier of (TOP-REAL n)) by A20;

then A22: f = 1_ (GFuncs the carrier of (TOP-REAL n)) by A21, GROUP_4:8

.= the_unity_wrt the multF of (GFuncs the carrier of (TOP-REAL n)) by GROUP_1:22

.= id (TOP-REAL n) by MONOID_0:75 ;

then rng f = [#] (TOP-REAL n) ;

then f is onto by FUNCT_2:def 3;

then f /" = f " by A22, TOPS_2:def 4;

hence ( ex k being Nat st

( k in dom F & ( for i, j being Nat

for r being Real holds

( not 1 <= i or not i < j or not j <= n or not F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) or f " is base_rotation ) by A22, FUNCT_1:45; :: thesis: verum

end;ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) holds

f " is base_rotation

let f be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( len F = 0 & Product F = f & ( for k being Nat st k in dom F holds

ex i, j being Nat ex r being Real st

( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) implies f " is base_rotation )

assume that

A20: len F = 0 and

A21: Product F = f ; :: thesis: ( ex k being Nat st

( k in dom F & ( for i, j being Nat

for r being Real holds

( not 1 <= i or not i < j or not j <= n or not F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) or f " is base_rotation )

F = <*> the carrier of (GFuncs the carrier of (TOP-REAL n)) by A20;

then A22: f = 1_ (GFuncs the carrier of (TOP-REAL n)) by A21, GROUP_4:8

.= the_unity_wrt the multF of (GFuncs the carrier of (TOP-REAL n)) by GROUP_1:22

.= id (TOP-REAL n) by MONOID_0:75 ;

then rng f = [#] (TOP-REAL n) ;

then f is onto by FUNCT_2:def 3;

then f /" = f " by A22, TOPS_2:def 4;

hence ( ex k being Nat st

( k in dom F & ( for i, j being Nat

for r being Real holds

( not 1 <= i or not i < j or not j <= n or not F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) or f " is base_rotation ) by A22, FUNCT_1:45; :: thesis: verum

then S

hence f " is base_rotation by A1; :: thesis: verum