let I be non empty set ; :: thesis: for F, G being Group-Family of I
for h being non empty Function
for x being Element of (product F)
for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
let F, G be Group-Family of I; :: thesis: for h being non empty Function
for x being Element of (product F)
for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
let h be non empty Function; :: thesis: for x being Element of (product F)
for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
let x be Element of (product F); :: thesis: for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
let y be Element of (product G); :: thesis: ( I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) implies for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) ) )
assume that
A1: I = dom h and
A2: y = (ProductMap ((Carrier F),(Carrier G),h)) . x and
A3: for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ; :: thesis: for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
set p = ProductMap ((Carrier F),(Carrier G),h);
dom (Carrier G) = I by PARTFUN1:def 2;
then A6: ( dom (Carrier F) = dom (Carrier G) & dom (Carrier G) = dom h ) by A1, PARTFUN1:def 2;
A7: for i being object st i in dom h holds
h . i is Function of ((Carrier F) . i),((Carrier G) . i)

proof

let i be object ; :: thesis: ( i in dom h implies h . i is Function of ((Carrier F) . i),((Carrier G) . i) )
assume i in dom h ; :: thesis: h . i is Function of ((Carrier F) . i),((Carrier G) . i)
then reconsider i = i as Element of I by A1;
A8: [#] (F . i) = (Carrier F) . i by PENCIL_3:7;
[#] (G . i) = (Carrier G) . i by PENCIL_3:7;
hence h . i is Function of ((Carrier F) . i),((Carrier G) . i) by A3, A8; :: thesis: verum

end;

for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )

proof

let i be Element of I; :: thesis: ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
reconsider x = x as Element of product (Carrier F) by GROUP_7:def 2;
consider hi being Function of ((Carrier F) . i),((Carrier G) . i) such that
A13: hi = h . i and
A14: ((ProductMap ((Carrier F),(Carrier G),h)) . x) . i = hi . (x . i) by A1, A6, A7, Def5;
hi is Homomorphism of (F . i),(G . i) by A3, A13;
hence ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) ) by A2, A13, A14; :: thesis: verum

end;

hence for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) ) ; :: thesis: verum