let a, b be Complex; :: thesis: {a} ++ {b} = {(a + b)}
let z be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not z in {a} ++ {b} or z in {(a + b)} ) & ( not z in {(a + b)} or z in {a} ++ {b} ) )
hereby :: thesis: ( not z in {(a + b)} or z in {a} ++ {b} )
assume z in {a} ++ {b} ; :: thesis: z in {(a + b)}
then consider c1, c2 being Complex such that
A1: z = c1 + c2 and
A2: ( c1 in {a} & c2 in {b} ) ;
( c1 = a & c2 = b ) by A2, TARSKI:def 1;
hence z in {(a + b)} by A1, TARSKI:def 1; :: thesis: verum
end;
A3: ( a in {a} & b in {b} ) by TARSKI:def 1;
assume z in {(a + b)} ; :: thesis: z in {a} ++ {b}
then A4: z = a + b by TARSKI:def 1;
thus z in {a} ++ {b} by A4, A3; :: thesis: verum