for f being PartFunc of REAL,REAL st dom f = REAL holds
R^1 | (R^1 (dom f)) = R^1