let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
x1,y1 are_summable
let x, y be Tuple of K, BOOLEAN ; :: thesis: for x1, y1 being Tuple of K + 1, BOOLEAN st x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
x1,y1 are_summable
let x1, y1 be Tuple of K + 1, BOOLEAN ; :: thesis: ( x1 = x ^ <*0*> & y1 = y ^ <*0*> implies x1,y1 are_summable )
set K1 = K + 1;
assume A1: ( x1 = x ^ <*0*> & y1 = y ^ <*0*> ) ; :: thesis: x1,y1 are_summable
A5: ( len x = K & len y = K ) by CARD_1:def 7;
A6: ( len x1 = K + 1 & len y1 = K + 1 ) by CARD_1:def 7;
A7: K + 1 in Seg (K + 1) by FINSEQ_1:4;
then K + 1 in dom x1 by FINSEQ_1:def 3, A6;
then x1 /. (K + 1) = x1 . (K + 1) by PARTFUN1:def 6;
then A3: x1 /. (K + 1) = 0 by FINSEQ_1:42, A1, A5;
K + 1 in dom y1 by FINSEQ_1:def 3, A6, A7;
then y1 /. (K + 1) = y1 . (K + 1) by PARTFUN1:def 6;
then (((x1 /. (K + 1)) '&' (y1 /. (K + 1))) 'or' ((x1 /. (K + 1)) '&' ((carry (x1,y1)) /. (K + 1)))) 'or' ((y1 /. (K + 1)) '&' ((carry (x1,y1)) /. (K + 1))) = 0 by A3, FINSEQ_1:42, A1, A5;
then add_ovfl (x1,y1) = FALSE by BINARITH:def 6;
hence x1,y1 are_summable by BINARITH:def 7; :: thesis: verum