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 "")) by Th35
.= (a ** (A "")) \+\ (a ** (B "")) by A1, Th200
.= (a /// A) \+\ (a /// B) ; :: thesis: verum