theorem Th39: :: RFUNCT_3:39

for D being non empty set
for F being PartFunc of D,REAL holds F " (right_closed_halfline 0) = (max- F) " {0}