theorem Th21: :: MATRIX_7:22

for G being Group
for f, g being FinSequence of G holds (f ^ g) " = (f ") ^ (g ")