:: deftheorem Def13 defines proj GROUP_23:def 13 :
for I being non empty set
for i being Element of I
for F being Group-Family of I
for b₄ being Homomorphism of (product F),(F . i) holds
( b₄ = proj (F,i) iff for h being Element of (product F) holds b₄ . h = h . i );