let A, B be complex-membered set ; :: thesis: for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a)
let a be complex number ; :: 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