theorem :: FUNCT_4:40

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