let M0 be multMagma-yielding Function; :: thesis: ( M0 = {} iff FreeAtoms M0 = {} )
A1: dom M0 = dom (Carrier M0) by PRALG_1:def 14;

hereby :: thesis: ( FreeAtoms M0 = {} implies M0 = {} )

assume M0 = {} ; :: thesis: FreeAtoms M0 = {}
then Carrier M0 = {} by A1;
then rng (disjoin (Carrier M0)) = {} by CARD_3:3;
then Union (disjoin (Carrier M0)) = {} by ZFMISC_1:2, CARD_3:def 4;
hence FreeAtoms M0 = {} ; :: thesis: verum

end;

assume A2: FreeAtoms M0 = {} ; :: thesis: M0 = {}
assume A3: M0 <> {} ; :: thesis: contradiction
then consider i being object such that
A4: i in dom M0 by XBOOLE_0:def 1;
reconsider i = i as Element of dom M0 by A4;
M0 . i in rng M0 by A4, FUNCT_1:3;
then reconsider R = M0 . i as non empty multMagma by GROUP_7:def 1;
set x = the Element of R;
the Element of R in the carrier of R ;
hence contradiction by A2, A3, Th8; :: thesis: verum