:: deftheorem Def41 defines <+> VALUED_2:def 41 :
for Y being complex-functions-membered set
for f being b1 -valued Function
for g being complex-valued Function
for b4 being Function holds
( b4 = f <+> g iff ( dom b4 = (dom f) /\ (dom g) & ( for x being object st x in dom b4 holds
b4 . x = (f . x) + (g . x) ) ) );