let c be Complex; :: thesis: for f being complex-valued Function holds c + f = ((dom f) --> c) + f
let f be complex-valued Function; :: thesis: c + f = ((dom f) --> c) + f
set g = (dom f) --> c;
A2: dom (c + f) = dom f by VALUED_1:def 2;
thus A3: dom (c + f) = (dom ((dom f) --> c)) /\ (dom f) by VALUED_1:def 2
.= dom (((dom f) --> c) + f) by VALUED_1:def 1 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (c + f) or (c + f) . b₁ = (((dom f) --> c) + f) . b₁ )
let x be object ; :: thesis: ( not x in dom (c + f) or (c + f) . x = (((dom f) --> c) + f) . x )
assume A4: x in dom (c + f) ; :: thesis: (c + f) . x = (((dom f) --> c) + f) . x
then A5: ((dom f) --> c) . x = c by A2, FUNCOP_1:7;
thus (c + f) . x = c + (f . x) by A4, VALUED_1:def 2
.= (((dom f) --> c) + f) . x by A3, A4, A5, VALUED_1:def 1 ; :: thesis: verum