thus for i being Element of INT holds addint . (0,i) = i :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: 0 is_a_right_unity_wrt addint

proof

let i be Element of INT ; :: thesis: addint . (0,i) = i
thus addint . (0,i) = 0 + i by Def20
.= i ; :: thesis: verum

end;

let i be Element of INT ; :: according to BINOP_1:def 17 :: thesis: addint . (i,0) = i
thus addint . (i,0) = i + 0 by Def20
.= i ; :: thesis: verum