let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN holds carry (x,y) = carry (y,x)
let x, y be Tuple of K, BOOLEAN ; :: thesis: carry (x,y) = carry (y,x)
A1: ( (carry (x,y)) /. 1 = FALSE & ( for i being Nat st 1 <= i & i < K holds
(carry (x,y)) /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' ((carry (x,y)) /. i))) 'or' ((y /. i) '&' ((carry (x,y)) /. i)) ) ) by BINARITH:def 2;
for i being Nat st 1 <= i & i < K holds
(carry (x,y)) /. (i + 1) = (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i))

proof

let i be Nat; :: thesis: ( 1 <= i & i < K implies (carry (x,y)) /. (i + 1) = (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i)) )
assume ( 1 <= i & i < K ) ; :: thesis: (carry (x,y)) /. (i + 1) = (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i))
hence (carry (x,y)) /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' ((carry (x,y)) /. i))) 'or' ((y /. i) '&' ((carry (x,y)) /. i)) by BINARITH:def 2
.= (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i)) ;
:: thesis: verum

end;

hence carry (x,y) = carry (y,x) by A1, BINARITH:def 2; :: thesis: verum