let M0, N0 be multMagma-yielding Function; :: thesis: ( M0 tolerates N0 implies FreeAtoms (M0 +* N0) = (FreeAtoms M0) \/ (FreeAtoms N0) )
A1: Carrier (M0 +* N0) = (Carrier M0) +* (Carrier N0) by PRALG_1:13;
A2: FreeAtoms (M0 +* N0) c= (FreeAtoms M0) \/ (FreeAtoms N0) by Th19;
assume A3: M0 tolerates N0 ; :: thesis: FreeAtoms (M0 +* N0) = (FreeAtoms M0) \/ (FreeAtoms N0)

now :: thesis: for i, x being object st [i,x] in (FreeAtoms M0) \/ (FreeAtoms N0) holds
[i,x] in FreeAtoms (M0 +* N0)

let i, x be object ; :: thesis: ( [i,x] in (FreeAtoms M0) \/ (FreeAtoms N0) implies [b₁,b₂] in FreeAtoms (M0 +* N0) )
assume [i,x] in (FreeAtoms M0) \/ (FreeAtoms N0) ; :: thesis: [b₁,b₂] in FreeAtoms (M0 +* N0)

per cases then ( [i,x] in FreeAtoms M0 or [i,x] in FreeAtoms N0 ) by XBOOLE_0:def 3;

suppose [i,x] in FreeAtoms M0 ; :: thesis: [b₁,b₂] in FreeAtoms (M0 +* N0)

then A4: ( i in dom M0 & x in (Carrier M0) . i ) by Th7;
then i in (dom M0) \/ (dom N0) by XBOOLE_0:def 3;
then A5: i in dom (M0 +* N0) by FUNCT_4:def 1;
i in dom (Carrier M0) by A4, PRALG_1:def 14;
then (Carrier (M0 +* N0)) . i = (Carrier M0) . i by A1, A3, PRALG_1:12, FUNCT_4:15;
hence [i,x] in FreeAtoms (M0 +* N0) by A4, A5, Th7; :: thesis: verum

end;

suppose [i,x] in FreeAtoms N0 ; :: thesis: [b₁,b₂] in FreeAtoms (M0 +* N0)

then A6: ( i in dom N0 & x in (Carrier N0) . i ) by Th7;
then i in (dom M0) \/ (dom N0) by XBOOLE_0:def 3;
then A7: i in dom (M0 +* N0) by FUNCT_4:def 1;
i in dom (Carrier N0) by A6, PRALG_1:def 14;
then x in (Carrier (M0 +* N0)) . i by A1, A6, FUNCT_4:13;
hence [i,x] in FreeAtoms (M0 +* N0) by A7, Th7; :: thesis: verum

end;

end;

end;

then (FreeAtoms M0) \/ (FreeAtoms N0) c= FreeAtoms (M0 +* N0) by RELAT_1:def 3;
hence FreeAtoms (M0 +* N0) = (FreeAtoms M0) \/ (FreeAtoms N0) by A2, XBOOLE_0:def 10; :: thesis: verum