theorem :: RFUNCT_3:45

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