let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN st x,y are_summable & x . (len x) = 1 holds
(x + y) . (len (x + y)) = 1
let x, y be Tuple of K, BOOLEAN ; :: thesis: ( x,y are_summable & x . (len x) = 1 implies (x + y) . (len (x + y)) = 1 )
assume AS: ( x,y are_summable & x . (len x) = 1 ) ; :: thesis: (x + y) . (len (x + y)) = 1
L0: len y = K by CARD_1:def 7;
1 <= len y by NAT_1:25;
then len y in Seg K by L0, FINSEQ_1:1;
then L1: len y in dom y by L0, FINSEQ_1:def 3;
R0: len x = K by CARD_1:def 7;
1 <= len x by NAT_1:25;
then PR2: len x in dom x by FINSEQ_3:25;
P1: y . (len y) = 0

proof

assume A1: y . (len y) <> 0 ; :: thesis: contradiction
y . (len y) in rng y by L1, FUNCT_1:3;
then y . (len y) in BOOLEAN by FINSEQ_1:def 4, TARSKI:def 3;
then y . (len y) = 1 by A1, MARGREL1:def 11, TARSKI:def 2;
hence contradiction by LMExtBit9, AS; :: thesis: verum

end;

P2: len (x + y) = K by CARD_1:def 7;
1 <= len (x + y) by NAT_1:25;
then P3: len (x + y) in Seg K by P2, FINSEQ_1:1;
then PP5: len (x + y) in dom (x + y) by P2, FINSEQ_1:def 3;
R3: x /. (len (x + y)) = 1 by PR2, P2, R0, AS, PARTFUN1:def 6;
L3: y /. (len (x + y)) = 0 by P2, L0, P1, L1, PARTFUN1:def 6;
K1: (carry (x,y)) /. (len (x + y)) = 0

proof

assume K2: not (carry (x,y)) /. (len (x + y)) = 0 ; :: thesis: contradiction
(carry (x,y)) /. (len (x + y)) = 1 by K2, MARGREL1:def 11, TARSKI:def 2;
then (((x /. (len (x + y))) '&' (y /. (len (x + y)))) 'or' ((x /. (len (x + y))) '&' ((carry (x,y)) /. (len (x + y))))) 'or' ((y /. (len (x + y))) '&' ((carry (x,y)) /. (len (x + y)))) = 1 by R3;
then add_ovfl (x,y) = 1 by P2, BINARITH:def 6;
hence contradiction by AS, BINARITH:def 7; :: thesis: verum

end;

(x + y) /. (len (x + y)) = ((x /. (len (x + y))) 'xor' (y /. (len (x + y)))) 'xor' ((carry (x,y)) /. (len (x + y))) by P3, BINARITH:def 5
.= 1 by L3, K1, PR2, P2, R0, AS, PARTFUN1:def 6 ;
hence (x + y) . (len (x + y)) = 1 by PP5, PARTFUN1:def 6; :: thesis: verum