:: deftheorem defines R_EAL MESFUNC5:def 7 :
for X being non empty set
for f being PartFunc of X,REAL holds R_EAL f = f;