let I be non empty set ; :: thesis: for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I
for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
let F, G be Group-Family of I; :: thesis: for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I
for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
let h be non empty Function; :: thesis: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) implies for i being Element of I
for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f) )
assume that
A1: I = dom h and
A2: for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ; :: thesis: for i being Element of I
for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
let i be Element of I; :: thesis: for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
let f be Element of (F . i); :: thesis: for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
let hi be Homomorphism of (F . i),(G . i); :: thesis: ( hi = h . i implies (SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f) )
assume A3: hi = h . i ; :: thesis: (SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
set x = (1ProdHom (F,i)) . f;
set y = (SumMap (F,G,h)) . ((1ProdHom (F,i)) . f);
(1ProdHom (F,i)) . f in ProjGroup (F,i) ;
then A6: (1ProdHom (F,i)) . f in sum F by GROUP_2:40;
reconsider x = (1ProdHom (F,i)) . f as Element of (product F) by GROUP_2:42;
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) in sum G by A6, FUNCT_2:5;
then reconsider y = (SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) as Element of (product G) by GROUP_2:42;
A8: x in dom (SumMap (F,G,h)) by A6, FUNCT_2:def 1;
SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F) by A1, A2, Def7;
then A10: y = (ProductMap (F,G,h)) . x by A8, FUNCT_1:47;
A11: dom y = I by Th3;
A13: x = (1_ (product F)) +* (i,f) by GROUP_12:def 3;
consider hi0 being Homomorphism of (F . i),(G . i) such that
A15: ( hi0 = h . i & y . i = hi0 . (x . i) ) by A1, A2, A10, Th39;
A16: y . i = hi . f by A3, A13, A15, GROUP_12:1;
A17: for j being Element of I st j <> i holds
y . j = 1_ (G . j)

proof

let j be Element of I; :: thesis: ( j <> i implies y . j = 1_ (G . j) )
assume j <> i ; :: thesis: y . j = 1_ (G . j)
then A18: x . j = 1_ (F . j) by A13, GROUP_12:1;
consider hj being Homomorphism of (F . j),(G . j) such that
A19: ( hj = h . j & y . j = hj . (x . j) ) by A1, A2, A10, Th39;
thus y . j = 1_ (G . j) by A18, A19, GROUP_6:31; :: thesis: verum

end;

y = (1_ (product G)) +* (i,(hi . f)) by A11, A16, A17, GROUP_12:1;
hence (SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f) by GROUP_12:def 3; :: thesis: verum