let A be complex-membered set ; :: thesis: for a being Complex holds a /// A = { (a / c) where c is Complex : c in A }
let a be Complex; :: thesis: a /// A = { (a / c) where c is Complex : c in A }
thus a /// A c= { (a / c) where c is Complex : c in A } :: according to XBOOLE_0:def 10 :: thesis: { (a / c) where c is Complex : c in A } c= a /// A

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in a /// A or e in { (a / c) where c is Complex : c in A } )
assume e in a /// A ; :: thesis: e in { (a / c) where c is Complex : c in A }
then consider c1, c2 being Complex such that
A1: e = c1 * c2 and
A2: ( c1 in {a} & c2 in A "" ) ;
A3: c1 * c2 = c1 / (c2 ") ;
( c2 " in A & c1 = a ) by A2, Th29, TARSKI:def 1;
hence e in { (a / c) where c is Complex : c in A } by A1, A3; :: thesis: verum

end;

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