thus multnat is commutative :: thesis: multnat is associative

proof

let n1 be Element of NAT ; :: according to BINOP_1:def 13 :: thesis: for b₁ being Element of NAT holds multnat . n1,b₁ = multnat . b₁,n1
let n2 be Element of NAT ; :: 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 be Element of NAT ; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of NAT holds multnat . n1,(multnat . b₁,b₂) = multnat . (multnat . n1,b₁),b₂
let n2, n3 be Element of NAT ; :: 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