:: deftheorem defines [* GR_FREE0:def 5 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for i being Element of I
for g being Element of (H . i) holds [*i,g*] = Class ((EqCl (ReductionRel H)),<*[i,g]*>);