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)
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 ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (f (#) (c1 + c2)) or (f (#) (c1 + c2)) . b1 = ((f (#) c1) + (f (#) c2)) . b1 )

let x be object ; :: thesis: ( not x in dom (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
.= ((f (#) c1) . x) + ((f (#) c2) . x) by
.= ((f (#) c1) + (f (#) c2)) . x by ;
:: thesis: verum