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