let G be non empty addMagma ; :: thesis: for A, B, C being Subset of G holds A + (B \/ C) = (A + B) \/ (A + C)
let A, B, C be Subset of G; :: thesis: A + (B \/ C) = (A + B) \/ (A + C)
thus A + (B \/ C) c= (A + B) \/ (A + C) :: according to XBOOLE_0:def 10 :: thesis: (A + B) \/ (A + 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 + B) \/ (A + C) )
assume x in A + (B \/ C) ; :: thesis: x in (A + B) \/ (A + C)
then consider g1, g2 being Element of G such that
A1: ( x = g1 + g2 & g1 in A ) and
A2: g2 in B \/ C ;
( g2 in B or g2 in C ) by A2, XBOOLE_0:def 3;
then ( x in A + B or x in A + C ) by A1;
hence x in (A + B) \/ (A + C) by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

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

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

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

end;

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

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

end;

end;

end;

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