y in REAL by XREAL_0:def 1;
hence the carrier of X --> y is RealMap of X by FUNCOP_1:45; :: thesis: verum