consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that
A1: f = Product F and
A2: 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;
consider G being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that
A3: g = Product G and
A4: for k being Nat st k in dom G holds
ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & G . k = Mx2Tran (Rotation (i,j,n,r)) ) by Def5;
f * g is base_rotation
proof
take GF = G ^ F; :: according to MATRTOP3:def 5 :: thesis: ( f * g = Product GF & ( for k being Nat st k in dom GF holds
ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) ) ) )
thus Product GF = (Product G) * (Product F) by GROUP_4:5
.= f * g by A3, A1, MONOID_0:70 ; :: thesis: for k being Nat st k in dom GF holds
ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) )
let k be Nat; :: thesis: ( k in dom GF implies ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) ) )
assume A5: k in dom GF ; :: thesis: ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) )
per cases ( k in dom G or ex m being Nat st
( m in dom F & k = (len G) + m ) ) by A5, FINSEQ_1:25;
suppose A6: k in dom G ; :: thesis: ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) )
then G . k = GF . k by FINSEQ_1:def 7;
hence ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) ) by A4, A6; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom F & k = (len G) + m ) ; :: thesis: ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) )
then consider m being Nat such that
A7: m in dom F and
A8: k = (len G) + m ;
GF . k = F . m by A7, A8, FINSEQ_1:def 7;
hence ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & GF . k = Mx2Tran (Rotation (i,j,n,r)) ) by A2, A7; :: thesis: verum
end;
end;
end;
hence for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 = f * g holds
b1 is base_rotation ; :: thesis: verum