let G1, G2 be Group; :: thesis: 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)) )
let phi be Homomorphism of G1,G2; :: thesis: 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)) )
let F1 be FinSequence of the carrier of G1; :: thesis: 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)) )
let ks be FinSequence of INT ; :: thesis: ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product (F2 |^ ks) = phi . (Product (F1 |^ ks)) )
consider F2 being FinSequence of the carrier of G2 such that
A2: ( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) ) by ThMappingFrobProd;
take F2 ; :: thesis: ( len F1 = len F2 & F2 = phi * F1 & Product (F2 |^ ks) = phi . (Product (F1 |^ ks)) )
thus ( len F1 = len F2 & F2 = phi * F1 ) by A2; :: thesis: Product (F2 |^ ks) = phi . (Product (F1 |^ ks))
A3: len (F1 |^ ks) = len F1 by GROUP_4:def 3
.= len (F2 |^ ks) by A2, GROUP_4:def 3 ;
A4: len (phi * (F1 |^ ks)) = len (F1 |^ ks) by FINSEQ_2:33;
for k being Nat st k in dom (F2 |^ ks) holds
(phi * (F1 |^ ks)) . k = (F2 |^ ks) . k

proof

let k be Nat; :: thesis: ( k in dom (F2 |^ ks) implies (phi * (F1 |^ ks)) . k = (F2 |^ ks) . k )
assume k in dom (F2 |^ ks) ; :: thesis: (phi * (F1 |^ ks)) . k = (F2 |^ ks) . k
then k in Seg (len (F1 |^ ks)) by A3, FINSEQ_1:def 3;
then B1: k in dom (F1 |^ ks) by FINSEQ_1:def 3;
then k in Seg (len (F1 |^ ks)) by FINSEQ_1:def 3;
then k in Seg (len F1) by GROUP_4:def 3;
then B2: k in dom F1 by FINSEQ_1:def 3;
then k in Seg (len F2) by A2, FINSEQ_1:def 3;
then B3: k in dom F2 by FINSEQ_1:def 3;
B4: ( F1 /. k in G1 & dom phi = the carrier of G1 ) by FUNCT_2:def 1;
set g = F1 /. k;
set n = @ (ks /. k);
(phi * (F1 |^ ks)) . k = phi . ((F1 |^ ks) . k) by B1, FUNCT_1:13
.= phi . ((F1 /. k) |^ (@ (ks /. k))) by B2, GROUP_4:def 3
.= (phi /. (F1 /. k)) |^ (@ (ks /. k)) by GROUP_6:37
.= ((phi * F1) /. k) |^ (@ (ks /. k)) by B2, B4, PARTFUN2:4
.= (F2 |^ ks) . k by A2, B3, GROUP_4:def 3 ;
hence (phi * (F1 |^ ks)) . k = (F2 |^ ks) . k ; :: thesis: verum

end;

hence Product (F2 |^ ks) = phi . (Product (F1 |^ ks)) by A3, A4, ThMappingFrobProdProperty, FINSEQ_2:9; :: thesis: verum