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

proof

let i be Element of INT ; :: thesis: multint . z,i = i
thus multint . z,i = 1 * i by Def22
.= i ; :: thesis: verum

end;

let i be Element of INT ; :: according to BINOP_1:def 17 :: thesis: multint . i,z = i
thus multint . i,z = i * 1 by Def22
.= i ; :: thesis: verum