thus multnat is commutative :: thesis: multnat is associative

proof

let n1, n2 be Element of NAT ; :: according to BINOP_1:def 13 :: thesis: multnat . n1,n2 = multnat . n2,n1
thus multnat . n1,n2 = n1 * n2 by Def24
.= multnat . n2,n1 by Def24 ; :: thesis: verum

end;

let n1, n2, n3 be Element of NAT ; :: according to BINOP_1:def 14 :: thesis: multnat . n1,(multnat . n2,n3) = multnat . (multnat . n1,n2),n3
thus multnat . n1,(multnat . n2,n3) = n1 * (multnat . n2,n3) by Def24
.= n1 * (n2 * n3) by Def24
.= (n1 * n2) * n3
.= (multnat . n1,n2) * n3 by Def24
.= multnat . (multnat . n1,n2),n3 by Def24 ; :: thesis: verum