thus addnat is commutative :: thesis: addnat is associative

proof

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