:: deftheorem Def1 defines +* FUNCT_4:def 1 :
for f, g, b₃ being Function holds
( b₃ = f +* g iff ( dom b₃ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b₃ . x = g . x ) & ( not x in dom g implies b₃ . x = f . x ) ) ) ) );