thus rng (R^1 f) = the carrier of (R^1 | (R^1 (rng f))) by PRE_TOPC:29; :: according to FUNCT_2:def 3 :: thesis: verum