set TR = TOP-REAL n;
set G = GFuncs the carrier of ();
defpred S1[ Nat] means for F being FinSequence of (GFuncs the carrier of ())
for f being Function of (),() 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 ()) 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 S1[i] holds
S1[i + 1]
proof
let z be Nat; :: thesis: ( S1[z] implies S1[z + 1] )
assume A3: S1[z] ; :: thesis: S1[z + 1]
set z1 = z + 1;
let F be FinSequence of (GFuncs the carrier of ()); :: thesis: for f being Function of (),() 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 (),(); :: 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:
set Fz = F | z;
reconsider fz = Product (F | z) as Function of (),() by MONOID_0:73;
1 <= z + 1 by NAT_1:11;
then z + 1 in dom F by ;
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 ()) by MONOID_0:73;
F = (F | z) ^ <*M*> by ;
then A9: f = (Product (F | z)) * M by
.= (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 ;
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))) = [#] () & Mx2Tran (Rotation (i,j,n,r)) is one-to-one & dom (Mx2Tran (Rotation (i,j,n,r))) = [#] () ) 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 ;
len (F | z) = z by ;
then A17: fz " is base_rotation by ;
( fz is one-to-one & dom fz = [#] () & rng fz = [#] () ) by ;
then A18: f " = (fz ") * ((Mx2Tran (Rotation (i,j,n,r))) ") by ;
Mx2Tran (Rotation (i,j,n,(- r))) is base_rotation by ;
hence f " is base_rotation by A14, A16, A17, A18; :: thesis: verum
end;
A19: S1[ 0 ]
proof
let F be FinSequence of (GFuncs the carrier of ()); :: thesis: for f being Function of (),() 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 (),(); :: 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 ()) by A20;
then A22: f = 1_ (GFuncs the carrier of ()) by
.= the_unity_wrt the multF of (GFuncs the carrier of ()) by GROUP_1:22
.= id () by MONOID_0:75 ;
then rng f = [#] () ;
then f is onto by FUNCT_2:def 3;
then f /" = f " by ;
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 ; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A19, A2);
then S1[ len F] ;
hence f " is base_rotation by A1; :: thesis: verum