thus addnat is commutative :: thesis: addnat is associative

proof

let n1, n2 be Element of NAT ; :: according to BINOP_1:def 2 :: thesis: addnat . (n1,n2) = addnat . (n2,n1)
thus addnat . (n1,n2) = n1 + n2 by Def23
.= addnat . (n2,n1) by Def23 ; :: thesis: verum

end;

let n1, n2, n3 be Element of NAT ; :: according to BINOP_1:def 3 :: thesis: addnat . (n1,(addnat . (n2,n3))) = addnat . ((addnat . (n1,n2)),n3)
thus addnat . (n1,(addnat . (n2,n3))) = n1 + (addnat . (n2,n3)) by Def23
.= n1 + (n2 + n3) by Def23
.= (n1 + n2) + n3
.= (addnat . (n1,n2)) + n3 by Def23
.= addnat . ((addnat . (n1,n2)),n3) by Def23 ; :: thesis: verum