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

hereby :: thesis: ( x in dom M0 & y in (Carrier M0) . x implies [x,y] in FreeAtoms M0 )

assume [x,y] in FreeAtoms M0 ; :: thesis: ( x in dom M0 & y in (Carrier M0) . x )
then ( x in dom (Carrier M0) & y in (Carrier M0) . x ) by WAYBEL26:38;
hence ( x in dom M0 & y in (Carrier M0) . x ) by PRALG_1:def 14; :: thesis: verum

end;

assume A1: ( x in dom M0 & y in (Carrier M0) . x ) ; :: thesis: [x,y] in FreeAtoms M0
then x in dom (Carrier M0) by PRALG_1:def 14;
hence [x,y] in FreeAtoms M0 by A1, WAYBEL26:38; :: thesis: verum