theorem Th47: :: GROUP_19:47

for G being Group
for F, F1, F2 being FinSequence of G st len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)