let A be complex-membered set ; :: thesis: for b, a being complex number st b in A holds
a * b in a ** A
let b, a be complex number ; :: thesis: ( b in A implies a * b in a ** A )
a in {a} by TARSKI:def 1;
hence ( b in A implies a * b in a ** A ) by Th89; :: thesis: verum