let A, B be complex-membered set ; :: thesis: for a being Complex holds (A -- B) /// a = (A /// a) -- (B /// a)
let a be Complex; :: thesis: (A -- B) /// a = (A /// a) -- (B /// a)
thus (A -- B) /// a = (A /// a) ++ ((-- B) /// a) by Th234
.= (A /// a) -- (B /// a) by Th94 ; :: thesis: verum