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

proof

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

end;

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