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;
MATRTOP3:def 5 ( 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
;
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;
( 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
;
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;
hence
for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 = f * g holds
b1 is base_rotation
; verum