:: deftheorem Def45 defines <++> VALUED_2:def 45 :
for Y1, Y2 being complex-functions-membered set
for f being b₁ -valued Function
for g being b₂ -valued Function
for b₅ being Function holds
( b₅ = f <++> g iff ( dom b₅ = (dom f) /\ (dom g) & ( for x being object st x in dom b₅ holds
b₅ . x = (f . x) + (g . x) ) ) );