theorem :: FUNCT_4:36

for X, Y being set
for f, g being PartFunc of X,Y st g is total holds
f +* g = g