let A be complex-membered set ; :: thesis: for a being complex number holds A -- a = { (c - a) where c is Element of COMPLEX : c in A }
let a be complex number ; :: thesis: A -- a = { (c - a) where c is Element of COMPLEX : c in A }
A1: A -- a = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in {a} ) } by Th71;
thus A -- a c= { (c - a) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def 10 :: thesis: { (c - a) where c is Element of COMPLEX : c in A } c= A -- a

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in A -- a or e in { (c - a) where c is Element of COMPLEX : c in A } )
assume e in A -- a ; :: thesis: e in { (c - a) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A2: e = c1 - c2 and
A3: c1 in A and
A4: c2 in {a} by A1;
c2 = a by A4, TARSKI:def 1;
hence e in { (c - a) where c is Element of COMPLEX : c in A } by A2, A3; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (c - a) where c is Element of COMPLEX : c in A } or e in A -- a )
assume e in { (c - a) where c is Element of COMPLEX : c in A } ; :: thesis: e in A -- a
then ex c being Element of COMPLEX st
( e = c - a & c in A ) ;
hence e in A -- a by Th182; :: thesis: verum