set p = ProductMap (F,G,h);
set s = (ProductMap (F,G,h)) | (sum F);
for y being object st y in rng ((ProductMap (F,G,h)) | (sum F)) holds
y in [#] (sum G)

proof

let y be object ; :: thesis: ( y in rng ((ProductMap (F,G,h)) | (sum F)) implies y in [#] (sum G) )
assume A4: y in rng ((ProductMap (F,G,h)) | (sum F)) ; :: thesis: y in [#] (sum G)
then consider x being object such that
A5: x in dom ((ProductMap (F,G,h)) | (sum F)) and
A6: y = ((ProductMap (F,G,h)) | (sum F)) . x by FUNCT_1:def 3;
dom ((ProductMap (F,G,h)) | (sum F)) c= dom (ProductMap (F,G,h)) by RELAT_1:60;
then x in dom (ProductMap (F,G,h)) by A5;
then reconsider x = x as Element of (product F) ;
reconsider y = y as Element of (product G) by A4;
A8: y = (ProductMap (F,G,h)) . x by A5, A6, FUNCT_1:47;
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i)

proof

let i be Element of I; :: thesis: ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i)
consider hi being Homomorphism of (F . i),(G . i) such that
A9: ( hi = h . i & y . i = hi . (x . i) ) by A1, A8, Th39;
thus ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) by A9; :: thesis: verum

end;

then support (y,G) c= support (x,F) by Th34;
then y in sum G by A5, Th8;
hence y in [#] (sum G) ; :: thesis: verum

end;

then rng ((ProductMap (F,G,h)) | (sum F)) c= [#] (sum G) ;
then [#] (Image ((ProductMap (F,G,h)) | (sum F))) c= [#] (sum G) by GROUP_6:44;
then A10: Image ((ProductMap (F,G,h)) | (sum F)) is Subgroup of sum G by GROUP_2:57;
(ProductMap (F,G,h)) | (sum F) is Homomorphism of (sum F),(Image ((ProductMap (F,G,h)) | (sum F))) by GROUP_6:49;
hence (ProductMap (F,G,h)) | (sum F) is Homomorphism of (sum F),(sum G) by A10, Th6; :: thesis: verum