theorem Th13: :: GR_FREE0:12

for M1, M2 being non empty multMagma holds FreeAtoms <*M1,M2*> = [:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]