[#] R^1 = R^1 ([#] REAL) by TOPMETR:17;
hence R^1 | (R^1 ([#] REAL)) = R^1 by PRE_TOPC:def 5; :: thesis: verum