let A, B, C be complex-membered set ; :: thesis: A ++ (B \/ C) = (A ++ B) \/ (A ++ C)
let a be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not a in A ++ (B \/ C) or a in (A ++ B) \/ (A ++ C) ) & ( not a in (A ++ B) \/ (A ++ C) or a in A ++ (B \/ C) ) )
hereby :: thesis: ( not a in (A ++ B) \/ (A ++ C) or a in A ++ (B \/ C) )
assume a in A ++ (B \/ C) ; :: thesis: a in (A ++ B) \/ (A ++ C)
then consider c, c1 being Complex such that
A1: a = c + c1 and
A2: c in A and
A3: c1 in B \/ C ;
( c1 in B or c1 in C ) by A3, XBOOLE_0:def 3;
then ( c + c1 in A ++ B or c + c1 in A ++ C ) by A2;
hence a in (A ++ B) \/ (A ++ C) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
assume A4: a in (A ++ B) \/ (A ++ C) ; :: thesis: a in A ++ (B \/ C)
per cases ( a in A ++ B or a in A ++ C ) by A4, XBOOLE_0:def 3;
suppose a in A ++ B ; :: thesis: a in A ++ (B \/ C)
then consider c, c1 being Complex such that
A5: ( a = c + c1 & c in A ) and
A6: c1 in B ;
c1 in B \/ C by A6, XBOOLE_0:def 3;
hence a in A ++ (B \/ C) by A5; :: thesis: verum
end;
suppose a in A ++ C ; :: thesis: a in A ++ (B \/ C)
then consider c, c1 being Complex such that
A7: ( a = c + c1 & c in A ) and
A8: c1 in C ;
c1 in B \/ C by A8, XBOOLE_0:def 3;
hence a in A ++ (B \/ C) by A7; :: thesis: verum
end;
end;