let G be non empty addMagma ; :: thesis: for A, B, C being Subset of G holds (A \/ B) + C = (A + C) \/ (B + C)
let A, B, C be Subset of G; :: thesis: (A \/ B) + C = (A + C) \/ (B + C)
thus (A \/ B) + C c= (A + C) \/ (B + C) :: according to XBOOLE_0:def 10 :: thesis: (A + C) \/ (B + C) c= (A \/ B) + C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A \/ B) + C or x in (A + C) \/ (B + C) )
assume x in (A \/ B) + C ; :: thesis: x in (A + C) \/ (B + C)
then consider g1, g2 being Element of G such that
A1: x = g1 + g2 and
A2: g1 in A \/ B and
A3: g2 in C ;
( g1 in A or g1 in B ) by A2, XBOOLE_0:def 3;
then ( x in A + C or x in B + C ) by A1, A3;
hence x in (A + C) \/ (B + C) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A + C) \/ (B + C) or x in (A \/ B) + C )
assume A4: x in (A + C) \/ (B + C) ; :: thesis: x in (A \/ B) + C

now :: thesis: x in (A \/ B) + C

per cases ( x in A + C or x in B + C ) by A4, XBOOLE_0:def 3;

suppose x in A + C ; :: thesis: x in (A \/ B) + C

then consider g1, g2 being Element of G such that
A5: x = g1 + g2 and
A6: g1 in A and
A7: g2 in C ;
g1 in A \/ B by A6, XBOOLE_0:def 3;
hence x in (A \/ B) + C by A5, A7; :: thesis: verum

end;

suppose x in B + C ; :: thesis: x in (A \/ B) + C

then consider g1, g2 being Element of G such that
A8: x = g1 + g2 and
A9: g1 in B and
A10: g2 in C ;
g1 in A \/ B by A9, XBOOLE_0:def 3;
hence x in (A \/ B) + C by A8, A10; :: thesis: verum

end;

end;

end;

hence x in (A \/ B) + C ; :: thesis: verum