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

proof

let n be Element of NAT ; :: thesis: multnat . (1,n) = n
thus multnat . (1,n) = 1 * n by Def24
.= n ; :: thesis: verum

end;

let n be Element of NAT ; :: according to BINOP_1:def 17 :: thesis: multnat . (n,1) = n
thus multnat . (n,1) = n * 1 by Def24
.= n ; :: thesis: verum