let A be complex-membered set ; :: thesis: for a, b being complex number holds (a - b) ** A c= (a ** A) -- (b ** A)
let a, b be complex number ; :: thesis: (a - b) ** A c= (a ** A) -- (b ** A)
{a} -- {b} = {(a - b)} by Th81;
hence (a - b) ** A c= (a ** A) -- (b ** A) by Th102; :: thesis: verum