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