theorem Th64: :: GR_FREE0:63

for I being non empty set
for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) st g <> 1_ (H . i) holds
nf [*i,g*] = <*[i,g]*>