let H be non empty addMagma ; :: thesis: for P, Q being Subset of H holds the addF of H .: [:P,Q:] = P + Q
let P, Q be Subset of H; :: thesis: the addF of H .: [:P,Q:] = P + Q
set f = the addF of H;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: P + Q c= the addF of H .: [:P,Q:]

let y be object ; :: thesis: ( y in the addF of H .: [:P,Q:] implies y in P + Q )
assume y in the addF of H .: [:P,Q:] ; :: thesis: y in P + Q
then consider x being object such that
x in [: the carrier of H, the carrier of H:] and
A1: x in [:P,Q:] and
A2: y = the addF of H . x by FUNCT_2:64;
consider a, b being object such that
A3: ( a in P & b in Q ) and
A4: x = [a,b] by A1, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of H by A3;
y = a + b by A2, A4;
hence y in P + Q by A3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in P + Q or y in the addF of H .: [:P,Q:] )
assume y in P + Q ; :: thesis: y in the addF of H .: [:P,Q:]
then consider g, h being Element of H such that
A5: y = g + h and
A6: ( g in P & h in Q ) ;
[g,h] in [:P,Q:] by A6, ZFMISC_1:87;
hence y in the addF of H .: [:P,Q:] by A5, FUNCT_2:35; :: thesis: verum