let M1 be non empty multMagma ; :: thesis: FreeAtoms <*M1*> = [:{1}, the carrier of M1:]
Union (disjoin (Carrier <*M1*>)) = Union (disjoin <* the carrier of M1*>) by PRALG_1:17
.= Union (disjoin {[1, the carrier of M1]}) by FINSEQ_1:def 5
.= Union (disjoin (1 .--> the carrier of M1)) by FUNCT_4:82
.= Union (1 .--> [: the carrier of M1,{1}:]) by CARD_3:4
.= Union {[1,[: the carrier of M1,{1}:]]} by FUNCT_4:82
.= union (rng {[1,[: the carrier of M1,{1}:]]}) by CARD_3:def 4
.= union {[: the carrier of M1,{1}:]} by RELAT_1:9
.= [: the carrier of M1,{1}:] by ZFMISC_1:25 ;
hence FreeAtoms <*M1*> = [:{1}, the carrier of M1:] by SYSREL:5; :: thesis: verum