let f be complex-valued Function; :: thesis: 0 + f = f
thus dom (0 + f) = dom f by VALUED_1:def 2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (0 + f) or (0 + f) . b₁ = f . b₁ )
let x be object ; :: thesis: ( not x in dom (0 + f) or (0 + f) . x = f . x )
assume x in dom (0 + f) ; :: thesis: (0 + f) . x = f . x
hence (0 + f) . x = 0 + (f . x) by VALUED_1:def 2
.= f . x ;
:: thesis: verum