theorem :: GR_FREE0:19

for M0, N0 being multMagma-yielding Function st M0 tolerates N0 holds
FreeAtoms (M0 +* N0) = (FreeAtoms M0) \/ (FreeAtoms N0)