let I be non empty set ; :: thesis: for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2 holds Image (product f) = product (Image f)
let F1, F2 be Group-Family of I; :: thesis: for f being Homomorphism-Family of F1,F2 holds Image (product f) = product (Image f)
let f be Homomorphism-Family of F1,F2; :: thesis: Image (product f) = product (Image f)
for g being Element of (product F2) holds
( g in Image (product f) iff g in product (Image f) )

proof

let g be Element of (product F2); :: thesis: ( g in Image (product f) iff g in product (Image f) )

hereby :: thesis: ( g in product (Image f) implies g in Image (product f) )

assume g in Image (product f) ; :: thesis: g in product (Image f)
then consider a being Element of (product F1) such that
A2: g = (product f) . a by GROUP_6:45;
A3: ( dom g = I & dom ((product f) . a) = I ) by GROUP_19:3;
for i being Element of I holds g . i in (Image f) . i

proof

let i be Element of I; :: thesis: g . i in (Image f) . i
B1: ( dom (product f) = the carrier of (product F1) & dom (proj (F1,i)) = the carrier of (product F1) ) by FUNCT_2:def 1;
B2: g . i = (proj (F2,i)) . ((product f) . a) by A2, Def13
.= ((proj (F2,i)) * (product f)) . a by B1, FUNCT_1:13 ;
((f . i) * (proj (F1,i))) . a = (f . i) . ((proj (F1,i)) . a) by B1, FUNCT_1:13
.= (f . i) . (a . i) by Def13 ;
then g . i = (f . i) . (a /. i) by B2, Def15;
then g . i in Image (f . i) by GROUP_6:45;
hence g . i in (Image f) . i by Def17; :: thesis: verum

end;

hence g in product (Image f) by A3, Th47; :: thesis: verum

end;

defpred S₁[ Element of I, object ] means ( $2 is Element of (F1 . $1) & g . $1 = (f . $1) . $2 );
assume A1: g in product (Image f) ; :: thesis: g in Image (product f)
A2: for i being Element of I ex ai being object st S₁[i,ai]

proof

let i be Element of I; :: thesis: ex ai being object st S₁[i,ai]
g . i in (Image f) . i by A1, GROUP_19:5;
then g . i in Image (f . i) by Def17;
then ex ai being Element of (F1 . i) st g . i = (f . i) . ai by GROUP_6:45;
hence ex ai being object st S₁[i,ai] ; :: thesis: verum

end;

consider a being ManySortedSet of I such that
A3: for i being Element of I holds S₁[i,a . i] from PBOOLE:sch 6(A2);
A4: dom a = I by PARTFUN1:def 2;
for i being Element of I holds a . i in F1 . i

proof

let i be Element of I; :: thesis: a . i in F1 . i
S₁[i,a . i] by A3;
hence a . i in F1 . i ; :: thesis: verum

end;

then a in product F1 by A4, Th47;
then reconsider a = a as Element of (product F1) ;
A5: ( dom g = I & dom ((product f) . a) = I ) by GROUP_19:3;
for i being Element of I holds g . i = ((product f) . a) . i

proof

let i be Element of I; :: thesis: g . i = ((product f) . a) . i
B1: ( dom (product f) = the carrier of (product F1) & dom (proj (F1,i)) = the carrier of (product F1) ) by FUNCT_2:def 1;
((product f) . a) . i = (proj (F2,i)) . ((product f) . a) by Def13
.= ((proj (F2,i)) * (product f)) . a by B1, FUNCT_1:13
.= ((f . i) * (proj (F1,i))) . a by Def15
.= (f . i) . ((proj (F1,i)) . a) by B1, FUNCT_1:13
.= (f . i) . (a . i) by Def13
.= g . i by A3 ;
hence g . i = ((product f) . a) . i ; :: thesis: verum

end;

then g = (product f) . a by A5;
hence g in Image (product f) by GROUP_6:45; :: thesis: verum

end;

hence Image (product f) = product (Image f) by GROUP_2:def 6; :: thesis: verum