let A be complex-membered set ; :: thesis: for a being complex number
for e being set st e in A /// a holds
ex c being Element of COMPLEX st
( e = c / a & c in A )
let a be complex number ; :: thesis: for e being set st e in A /// a holds
ex c being Element of COMPLEX st
( e = c / a & c in A )
let e be set ; :: thesis: ( e in A /// a implies ex c being Element of COMPLEX st
( e = c / a & c in A ) )
A /// a = { (c / a) where c is Element of COMPLEX : c in A } by Th233;
hence ( e in A /// a implies ex c being Element of COMPLEX st
( e = c / a & c in A ) ) ; :: thesis: verum