theorem Th8: :: GR_FREE0:7

for x being object
for M being non empty multMagma-yielding Function
for i being Element of dom M holds
( [i,x] in FreeAtoms M iff x in the carrier of (M . i) )