theorem Th46: :: GROUP_19:46

for G being Group
for h being Element of G
for F being FinSequence of G st ( for k being Nat st k in dom F holds
h * (F /. k) = (F /. k) * h ) holds
h * (Product F) = (Product F) * h