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