theorem :: MATRIX_7:20

for G being Group
for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")