reconsider y = x as Element of REAL by XREAL_0:def 1;
multreal [;] (y,(id REAL)) is UnOp of REAL ;
hence multreal [;] (x,(id REAL)) is UnOp of REAL ; :: thesis: verum