A1: the carrier of (R^1 | (R^1 (rng f))) = R^1 (rng f) by PRE_TOPC:29;
the carrier of (R^1 | (R^1 (dom f))) = R^1 (dom f) by PRE_TOPC:29;
hence f is Function of (R^1 | (R^1 (dom f))),(R^1 | (R^1 (rng f))) by A1, FUNCT_2:4; :: thesis: verum