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 Th75;
hence (a - b) /// A c= (a /// A) -- (b /// A) by Th96; :: thesis: verum