thus addnat is commutative :: thesis: addnat is associative

proof

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