:: deftheorem Def1 defines ProjSet GROUP_12:def 1 :
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 Subset of (product F) holds
( b₄ = ProjSet (F,i) iff for x being set holds
( x in b₄ iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) );