thus for w being Element of RAT holds addrat . (0,w) = w :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: 0 is_a_right_unity_wrt addrat

proof

let w be Element of RAT ; :: thesis: addrat . (0,w) = w
thus addrat . (0,w) = 0 + w by Def15
.= w ; :: thesis: verum

end;

let w be Element of RAT ; :: according to BINOP_1:def 17 :: thesis: addrat . (w,0) = w
thus addrat . (w,0) = w + 0 by Def15
.= w ; :: thesis: verum