let f be PartFunc of REAL,REAL; :: thesis: ( dom f = REAL implies R^1 | (R^1 (dom f)) = R^1 )
assume dom f = REAL ; :: thesis: R^1 | (R^1 (dom f)) = R^1
then [#] R^1 = R^1 (dom f) by TOPMETR:17;
hence R^1 | (R^1 (dom f)) = R^1 by PRE_TOPC:def 5; :: thesis: verum