let X be set ; :: thesis: for M1 being non empty multMagma holds FreeAtoms (X --> M1) = [:X, the carrier of M1:]
let M1 be non empty multMagma ; :: thesis: FreeAtoms (X --> M1) = [:X, the carrier of M1:]
Union (disjoin (Carrier (X --> M1))) = Union (disjoin (X --> the carrier of M1)) by PRALG_1:16
.= [: the carrier of M1,X:] by CARD_3:25 ;
hence FreeAtoms (X --> M1) = [:X, the carrier of M1:] by SYSREL:5; :: thesis: verum