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