let A, B be complex-membered set ; :: thesis: for a being Complex holds
( A c= B iff a ++ A c= a ++ B )
let a be Complex; :: thesis: ( A c= B iff a ++ A c= a ++ B )
thus ( A c= B implies a ++ A c= a ++ B ) by Th47; :: thesis: ( a ++ A c= a ++ B implies A c= B )
assume A1: a ++ A c= a ++ B ; :: thesis: A c= B
let z be Complex; :: according to MEMBERED:def 7 :: thesis: ( not z in A or z in B )
assume z in A ; :: thesis: z in B
then a + z in a ++ A by Th141;
then ex c being Complex st
( a + z = a + c & c in B ) by A1, Th143;
hence z in B ; :: thesis: verum