:: deftheorem Def3 defines 1ProdHom GROUP_12:def 3 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b₄ being Homomorphism of (F . i),(ProjGroup (F,i)) holds
( b₄ = 1ProdHom (F,i) iff for x being Element of (F . i) holds b₄ . x = (1_ (product F)) +* (i,x) );