let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN st y = 0* K holds
( x + y = x & y + x = x )
let x, y be Tuple of K, BOOLEAN ; :: thesis: ( y = 0* K implies ( x + y = x & y + x = x ) )
assume AS: y = 0* K ; :: thesis: ( x + y = x & y + x = x )
for i being Nat st i in Seg K holds
(x + y) . i = x . i

proof

let i be Nat; :: thesis: ( i in Seg K implies (x + y) . i = x . i )
assume A1: i in Seg K ; :: thesis: (x + y) . i = x . i
then A4: ( 1 <= i & i <= K & i <> 0 ) by FINSEQ_1:1;
A2: y /. i = 0 by AS, A4, LMExtBit4;
A3: (carry (x,y)) /. i = 0 by AS, A4, LMExtBit3;
len x = K by CARD_1:def 7;
then D1: dom x = Seg K by FINSEQ_1:def 3;
len (x + y) = K by CARD_1:def 7;
then D2: dom (x + y) = Seg K by FINSEQ_1:def 3;
thus (x + y) . i = (x + y) /. i by D2, A1, PARTFUN1:def 6
.= ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) by BINARITH:def 5, A1
.= x . i by D1, A1, PARTFUN1:def 6, A2, A3 ; :: thesis: verum

end;

hence x + y = x by FINSEQ_2:119; :: thesis: y + x = x
hence y + x = x by LMExtBit500; :: thesis: verum