let G1, G2 be Group; :: thesis: for phi being Homomorphism of G1,G2
for F1 being FinSequence of the carrier of G1
for F2 being FinSequence of the carrier of G2 st F2 = phi * F1 holds
Product F2 = phi . (Product F1)
let phi be Homomorphism of G1,G2; :: thesis: for F1 being FinSequence of the carrier of G1
for F2 being FinSequence of the carrier of G2 st F2 = phi * F1 holds
Product F2 = phi . (Product F1)
let F1 be FinSequence of the carrier of G1; :: thesis: for F2 being FinSequence of the carrier of G2 st F2 = phi * F1 holds
Product F2 = phi . (Product F1)
let F2 be FinSequence of the carrier of G2; :: thesis: ( F2 = phi * F1 implies Product F2 = phi . (Product F1) )
assume A2: F2 = phi * F1 ; :: thesis: Product F2 = phi . (Product F1)
set n1 = len F1;
defpred S₁[ FinSequence of the carrier of G1] means phi . (Product $1) = Product (phi * $1);
A3: S₁[ <*> the carrier of G1]

proof

phi . (Product (<*> the carrier of G1)) = phi . (1_ G1) by GROUP_4:8
.= 1_ G2 by GROUP_6:31
.= Product (<*> the carrier of G2) by GROUP_4:8 ;
hence S₁[ <*> the carrier of G1] ; :: thesis: verum

end;

A4: for p0 being FinSequence of the carrier of G1
for x being Element of the carrier of G1 st S₁[p0] holds
S₁[p0 ^ <*x*>]

proof

let p0 be FinSequence of the carrier of G1; :: thesis: for x being Element of the carrier of G1 st S₁[p0] holds
S₁[p0 ^ <*x*>]
let x be Element of the carrier of G1; :: thesis: ( S₁[p0] implies S₁[p0 ^ <*x*>] )
assume B1: S₁[p0] ; :: thesis: S₁[p0 ^ <*x*>]
Product (p0 ^ <*x*>) = (Product p0) * x by GROUP_4:6;
then phi . (Product (p0 ^ <*x*>)) = (phi . (Product p0)) * (phi . x) by GROUP_6:def 6
.= Product ((phi * p0) ^ <*(phi . x)*>) by B1, GROUP_4:6 ;
hence S₁[p0 ^ <*x*>] by FINSEQOP:8; :: thesis: verum

end;

A5: for p0 being FinSequence of the carrier of G1 holds S₁[p0] from FINSEQ_2:sch 2(A3, A4);
thus Product F2 = phi . (Product F1) by A2, A5; :: thesis: verum