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

proof

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

end;

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