theorem Th55: :: GR_FREE0:54

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