theorem Th7: :: GR_FREE0:6

for x, y being object
for M0 being multMagma-yielding Function holds
( [x,y] in FreeAtoms M0 iff ( x in dom M0 & y in (Carrier M0) . x ) )