reconsider y = x as 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