let M1, M2, M3 be non empty multMagma ; FreeAtoms <*M1,M2,M3*> = ([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) \/ [:{3}, the carrier of M3:]
set S1 = [: the carrier of M1,{1}:];
set S2 = [: the carrier of M2,{2}:];
set S3 = [: the carrier of M3,{3}:];
set T1 = [:{1}, the carrier of M1:];
set T2 = [:{2}, the carrier of M2:];
set T3 = [:{3}, the carrier of M3:];
Union (disjoin (Carrier <*M1,M2,M3*>)) =
Union (disjoin <* the carrier of M1, the carrier of M2, the carrier of M3*>)
by PRALG_1:19
.=
Union <*[: the carrier of M1,{1}:],[: the carrier of M2,{2}:],[: the carrier of M3,{3}:]*>
by FINSEQ_3:162
.=
union (rng <*[: the carrier of M1,{1}:],[: the carrier of M2,{2}:],[: the carrier of M3,{3}:]*>)
by CARD_3:def 4
.=
union {[: the carrier of M1,{1}:],[: the carrier of M2,{2}:],[: the carrier of M3,{3}:]}
by FINSEQ_2:128
.=
union ({[: the carrier of M1,{1}:],[: the carrier of M2,{2}:]} \/ {[: the carrier of M3,{3}:]})
by ENUMSET1:3
.=
(union {[: the carrier of M1,{1}:],[: the carrier of M2,{2}:]}) \/ (union {[: the carrier of M3,{3}:]})
by ZFMISC_1:78
.=
([: the carrier of M1,{1}:] \/ [: the carrier of M2,{2}:]) \/ (union {[: the carrier of M3,{3}:]})
by ZFMISC_1:75
.=
([: the carrier of M1,{1}:] \/ [: the carrier of M2,{2}:]) \/ [: the carrier of M3,{3}:]
by ZFMISC_1:25
.=
(([:{1}, the carrier of M1:] ~) \/ [: the carrier of M2,{2}:]) \/ [: the carrier of M3,{3}:]
by SYSREL:5
.=
(([:{1}, the carrier of M1:] ~) \/ ([:{2}, the carrier of M2:] ~)) \/ [: the carrier of M3,{3}:]
by SYSREL:5
.=
(([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) ~) \/ [: the carrier of M3,{3}:]
by RELAT_1:23
.=
(([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) ~) \/ ([:{3}, the carrier of M3:] ~)
by SYSREL:5
.=
(([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) \/ [:{3}, the carrier of M3:]) ~
by RELAT_1:23
;
hence
FreeAtoms <*M1,M2,M3*> = ([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) \/ [:{3}, the carrier of M3:]
; verum