let c1, c2 be complex number ; :: 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)
A1: dom (f (#) (c1 + c2)) = dom f by VALUED_1:def 5;
A2: dom (f (#) c1) = dom f by VALUED_1:def 5;
A3: dom (f (#) c2) = dom f by VALUED_1:def 5;
A4: dom ((f (#) c1) + (f (#) c2)) = (dom (f (#) c1)) /\ (dom (f (#) c2)) by VALUED_1:def 1;
hence dom (f (#) (c1 + c2)) = dom ((f (#) c1) + (f (#) c2)) by A2, A3, VALUED_1:def 5; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (f (#) (c1 + c2)) or (f (#) (c1 + c2)) . b₁ = ((f (#) c1) + (f (#) c2)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (f (#) (c1 + c2)) or (f (#) (c1 + c2)) . x = ((f (#) c1) + (f (#) c2)) . x )
assume A5: x in dom (f (#) (c1 + c2)) ; :: thesis: (f (#) (c1 + c2)) . x = ((f (#) c1) + (f (#) c2)) . x
hence (f (#) (c1 + c2)) . x = (f . x) * (c1 + c2) by VALUED_1:def 5
.= ((f . x) * c1) + ((f . x) * c2)
.= ((f (#) c1) . x) + ((f . x) * c2) by A1, A2, A5, VALUED_1:def 5
.= ((f (#) c1) . x) + ((f (#) c2) . x) by A1, A3, A5, VALUED_1:def 5
.= ((f (#) c1) + (f (#) c2)) . x by A1, A2, A3, A4, A5, VALUED_1:def 1 ;
:: thesis: verum