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 (F,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 (F,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 (F,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 (F,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 (F,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 (F,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) )
y = (ProductMap ((Carrier F),(Carrier G),h)) . x by A1, A2, A3, Def6;
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) ) by A1, A3, Th38; :: thesis: verum