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