:: deftheorem Def888 defines + FINANCE5:def 2 :
for f1, f2 being ext-real-valued Function
for b₃ being Function holds
( b₃ = f1 + f2 iff ( dom b₃ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₃ holds
b₃ . x = (f1 . x) + (f2 . x) ) ) );