:: deftheorem defines + MESFUNC1:def 3 :
for C being non empty set
for f1, f2 being b₁ -defined ExtREAL -valued Function
for b₄ being PartFunc of C,ExtREAL holds
( b₄ = f1 + f2 iff ( dom b₄ = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b₄ holds
b₄ . c = (f1 . c) + (f2 . c) ) ) );