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