theorem ThMappingFrobProd2: :: GROUP_23:8

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