let A, B be complex-membered set ; :: thesis: for a being Complex st a <> 0 holds
a ** (A \+\ B) = (a ** A) \+\ (a ** B)
let a be Complex; :: thesis: ( a <> 0 implies a ** (A \+\ B) = (a ** A) \+\ (a ** B) )
assume A1: a <> 0 ; :: thesis: a ** (A \+\ B) = (a ** A) \+\ (a ** B)
thus a ** (A \+\ B) = (a ** (A \ B)) \/ (a ** (B \ A)) by Th92
.= ((a ** A) \ (a ** B)) \/ (a ** (B \ A)) by A1, Th199
.= (a ** A) \+\ (a ** B) by A1, Th199 ; :: thesis: verum