:: deftheorem Def2 defines + VALUED_1:def 2 :
for f being complex-valued Function
for r being Complex
for b₃ being Function holds
( b₃ = r + f iff ( dom b₃ = dom f & ( for c being object st c in dom b₃ holds
b₃ . c = r + (f . c) ) ) );