thus for n being Element of NAT holds addnat . (0,n) = n :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: 0 is_a_right_unity_wrt addnat

proof

let n be Element of NAT ; :: thesis: addnat . (0,n) = n
thus addnat . (0,n) = 0 + n by Def23
.= n ; :: thesis: verum

end;

let n be Element of NAT ; :: according to BINOP_1:def 17 :: thesis: addnat . (n,0) = n
thus addnat . (n,0) = n + 0 by Def23
.= n ; :: thesis: verum