consider F being FinSequence of (GFuncs the carrier of ()) 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 ()) 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 = () * () by GROUP_4:5
.= f * g by ; :: 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 ;
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 ;
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 (),() st b1 = f * g holds
b1 is base_rotation ; :: thesis: verum