theorem :: MESFUNC9:5

for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V123() & g is V124() holds
f - g is V123()