theorem Th40: :: RFUNCT_3:40

for D being non empty set
for F being PartFunc of D,REAL
for d being Element of D holds 0 <= (max- F) . d