theorem Th2: :: GROUP_12:2

for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )