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