let c, d be Complex; :: thesis: for f being complex-valued Function holds (c - d) (#) f = (c (#) f) - (d (#) f)
let f be complex-valued Function; :: thesis: (c - d) (#) f = (c (#) f) - (d (#) f)
dom ((c (#) f) - (d (#) f)) = (dom (c (#) f)) /\ (dom (d (#) f)) by VALUED_1:12
.= (dom f) /\ (dom (d (#) f)) by VALUED_1:def 5
.= (dom f) /\ (dom f) by VALUED_1:def 5 ;
hence A1: dom ((c - d) (#) f) = dom ((c (#) f) - (d (#) f)) by VALUED_1:def 5; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom ((c - d) (#) f) or ((c - d) (#) f) . b₁ = ((c (#) f) - (d (#) f)) . b₁ )
let x be object ; :: thesis: ( not x in dom ((c - d) (#) f) or ((c - d) (#) f) . x = ((c (#) f) - (d (#) f)) . x )
assume A2: x in dom ((c - d) (#) f) ; :: thesis: ((c - d) (#) f) . x = ((c (#) f) - (d (#) f)) . x
thus ((c - d) (#) f) . x = (c - d) * (f . x) by VALUED_1:6
.= (c * (f . x)) - (d * (f . x))
.= (c * (f . x)) - ((d (#) f) . x) by VALUED_1:6
.= ((c (#) f) . x) - ((d (#) f) . x) by VALUED_1:6
.= ((c (#) f) - (d (#) f)) . x by A1, A2, VALUED_1:13 ; :: thesis: verum