theorem Th54: :: GR_FREE0:53

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> = (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g