theorem Th1: :: GROUP_12:1

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