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 ;
( 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))
;
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)
then
support (
y,
G)
c= support (
x,
F)
by Th34;
then
y in sum G
by A5, Th8;
hence
y in [#] (sum G)
;
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; verum