let M1, M2 be non empty multMagma ; FreeAtoms <*M1,M2*> = [:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]
set S1 = [: the carrier of M1,{1}:];
set S2 = [: the carrier of M2,{2}:];
Union (disjoin (Carrier <*M1,M2*>)) =
Union (disjoin <* the carrier of M1, the carrier of M2*>)
by PRALG_1:18
.=
Union <*[: the carrier of M1,{1}:],[: the carrier of M2,{2}:]*>
by FINSEQ_3:161
.=
union (rng <*[: the carrier of M1,{1}:],[: the carrier of M2,{2}:]*>)
by CARD_3:def 4
.=
union {[: the carrier of M1,{1}:],[: the carrier of M2,{2}:]}
by FINSEQ_2:127
.=
[: the carrier of M1,{1}:] \/ [: the carrier of M2,{2}:]
by ZFMISC_1:75
.=
([:{1}, the carrier of M1:] ~) \/ [: the carrier of M2,{2}:]
by SYSREL:5
.=
([:{1}, the carrier of M1:] ~) \/ ([:{2}, the carrier of M2:] ~)
by SYSREL:5
.=
([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) ~
by RELAT_1:23
;
hence
FreeAtoms <*M1,M2*> = [:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]
; verum