thus for r being Element of REAL holds addreal . ((In (0,REAL)),r) = r :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: In (0,REAL) is_a_right_unity_wrt addreal

proof

let r be Element of REAL ; :: thesis: addreal . ((In (0,REAL)),r) = r
thus addreal . ((In (0,REAL)),r) = 0 + r by Def9
.= r ; :: thesis: verum

end;

let r be Element of REAL ; :: according to BINOP_1:def 17 :: thesis: addreal . (r,(In (0,REAL))) = r
thus addreal . (r,(In (0,REAL))) = r + 0 by Def9
.= r ; :: thesis: verum