let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN holds x + y = y + x
let x, y be Tuple of K, BOOLEAN ; :: thesis: x + y = y + x
for i being Nat st i in Seg K holds
(x + y) /. i = ((y /. i) 'xor' (x /. i)) 'xor' ((carry (y,x)) /. i)

proof

let i be Nat; :: thesis: ( i in Seg K implies (x + y) /. i = ((y /. i) 'xor' (x /. i)) 'xor' ((carry (y,x)) /. i) )
assume i in Seg K ; :: thesis: (x + y) /. i = ((y /. i) 'xor' (x /. i)) 'xor' ((carry (y,x)) /. i)
then (x + y) /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) by BINARITH:def 5;
hence (x + y) /. i = ((y /. i) 'xor' (x /. i)) 'xor' ((carry (y,x)) /. i) by LMExtBit501; :: thesis: verum

end;

hence x + y = y + x by BINARITH:def 5; :: thesis: verum