:: deftheorem defines R^1 TOPREALB:def 4 :
for f being PartFunc of REAL,REAL holds R^1 f = f;