theorem ThMappingFrobProd: :: GROUP_23:7

for G1, G2 being Group
for phi being Homomorphism of G1,G2
for F1 being FinSequence of the carrier of G1 ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) )