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