let A be complex-membered set ; :: thesis: 0 ++ A = A
let a be complex number ; :: 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 Element of 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;

A4: a in COMPLEX by XCMPLX_0:def 2;
assume a in A ; :: thesis: a in 0 ++ A
then 0 + a in { (0 + c) where c is Element of COMPLEX : c in A } by A4;
hence a in 0 ++ A by Th142; :: thesis: verum