theorem :: RFUNCT_3:57

for F being PartFunc of REAL,REAL
for X being set st X c= dom F holds
0 (#) F is_convex_on X