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

end;

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