let c1, c2 be Complex; :: thesis: for f being complex-valued Function holds f (#) (c1 - c2) = (f (#) c1) - (f (#) c2)
let f be complex-valued Function; :: thesis: f (#) (c1 - c2) = (f (#) c1) - (f (#) c2)
thus f (#) (c1 - c2) = (f (#) c1) + (f (#) (- c2)) by Th2
.= (f (#) c1) - (f (#) c2) by VALUED_2:24 ; :: thesis: verum