1 in NAT ;
then reconsider j = 1 as Element of REAL by NUMBERS:19;
thus for r being Element of REAL holds multreal . (1,r) = r :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: 1 is_a_right_unity_wrt multreal

proof

let r be Element of REAL ; :: thesis: multreal . (1,r) = r
thus multreal . (1,r) = 1 * r by Def11
.= r ; :: thesis: verum

end;

let r be Element of REAL ; :: according to BINOP_1:def 17 :: thesis: multreal . (r,1) = r
thus multreal . (r,1) = r * 1 by Def11
.= r ; :: thesis: verum