let A be complex-membered set ; :: thesis: 0 ++ A = A
let a be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not a in 0 ++ A or a in A ) & ( not a in A or a in 0 ++ A ) )

hereby :: thesis: ( not a in A or a in 0 ++ A )

assume a in 0 ++ A ; :: thesis: a in A
then consider c1, c2 being Complex such that
A1: a = c1 + c2 and
A2: c1 in {0} and
A3: c2 in A ;
c1 = 0 by A2, TARSKI:def 1;
hence a in A by A1, A3; :: thesis: verum

end;

assume a in A ; :: thesis: a in 0 ++ A
then 0 + a in { (0 + c) where c is Complex : c in A } ;
hence a in 0 ++ A by Th142; :: thesis: verum