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_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} = f * g holds

b_{1} is base_rotation
; :: thesis: verum

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

hence
for b
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)) )

end;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;

end;

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

( 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;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

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

( 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;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

b