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

proof

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

end;

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