let M be non empty multMagma-yielding Function; :: thesis: FreeAtoms M = union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum }
set S = { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } ;

now :: thesis: for z being object holds
( ( z in FreeAtoms M implies z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } ) & ( z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } implies z in FreeAtoms M ) )

let z be object ; :: thesis: ( ( z in FreeAtoms M implies z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } ) & ( z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } implies z in FreeAtoms M ) )

hereby :: thesis: ( z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } implies z in FreeAtoms M )

assume A1: z in FreeAtoms M ; :: thesis: z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum }
then consider i, g being object such that
A2: z = [i,g] by RELAT_1:def 1;
reconsider i = i as Element of dom M by A1, A2, Th7;
A3: g in the carrier of (M . i) by A1, A2, Th8;
i in {i} by TARSKI:def 1;
then A4: z in [:{i}, the carrier of (M . i):] by A2, A3, ZFMISC_1:def 2;
[:{i}, the carrier of (M . i):] in { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } ;
hence z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } by A4, TARSKI:def 4; :: thesis: verum

end;

assume z in union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } ; :: thesis: z in FreeAtoms M
then consider Z being set such that
A5: ( z in Z & Z in { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } ) by TARSKI:def 4;
consider i being Element of dom M such that
A6: Z = [:{i}, the carrier of (M . i):] by A5;
consider j, g being object such that
A7: ( j in {i} & g in the carrier of (M . i) & z = [j,g] ) by A5, A6, ZFMISC_1:def 2;
z = [i,g] by A7, TARSKI:def 1;
hence z in FreeAtoms M by A7, Th8; :: thesis: verum

end;

hence FreeAtoms M = union { [:{i}, the carrier of (M . i):] where i is Element of dom M : verum } by TARSKI:2; :: thesis: verum