theorem Th11: :: GR_FREE0:10

for M being non empty multMagma-yielding Function holds FreeAtoms M = union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum }