the carrier of (T | X) = X by PRE_TOPC:29;
hence f | X is RealMap of (T | X) by FUNCT_2:38; :: thesis: verum