set TR = TOP-REAL n;
set G = GFuncs the carrier of (TOP-REAL n);
defpred S₁[ 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₁[i] holds
S₁[i + 1]

proof

let z be Nat; :: thesis: ( S₁[z] implies S₁[z + 1] )
assume A3: S₁[z] ; :: thesis: S₁[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;

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

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;

then A13: fz is base_rotation ;
( 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;

A19: S₁[ 0 ]

proof

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;

for i being Nat holds S₁[i] from NAT_1:sch 2(A19, A2);
then S₁[ len F] ;
hence f " is base_rotation by A1; :: thesis: verum