thus multnat is commutative :: thesis: multnat is associative

proof

let n1, n2 be Element of NAT ; :: according to BINOP_1:def 2 :: 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 3 :: 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