theorem Th44: :: RFUNCT_3:44

for D being non empty set
for F being PartFunc of D,REAL
for X being set holds (max+ F) | X = max+ (F | X)