let A be complex-membered set ; :: thesis: for a being complex number holds a /// A = { (a / c) where c is Element of COMPLEX : c in A }
let a be complex number ; :: thesis: a /// A = { (a / c) where c is Element of COMPLEX : c in A }
thus a /// A c= { (a / c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def 10 :: thesis: { (a / c) 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 { (a / c) where c is Element of COMPLEX : c in A } )
assume e in a /// A ; :: thesis: e in { (a / c) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 * c2 and
A2: c1 in {a} and
A3: c2 in A "" ;
A4: c2 " in A by A3, Th35;
A5: c1 * c2 = c1 / (c2 " ) ;
c1 = a by A2, TARSKI:def 1;
hence e in { (a / c) where c is Element of COMPLEX : c in A } by A1, A4, A5; :: thesis: verum

end;

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