let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN st x . (len x) = 1 & y . (len y) = 1 holds
not x,y are_summable
let x, y be Tuple of K, BOOLEAN ; :: thesis: ( x . (len x) = 1 & y . (len y) = 1 implies not x,y are_summable )
assume AS: ( x . (len x) = 1 & y . (len y) = 1 ) ; :: thesis: not x,y are_summable
A5: ( len x = K & len y = K ) by CARD_1:def 7;
1 <= len x by NAT_1:25;
then len x in dom x by FINSEQ_3:25;
then A6: x /. K = 1 by AS, A5, PARTFUN1:def 6;
1 <= len y by NAT_1:25;
then len y in dom y by FINSEQ_3:25;
then A7: y /. K = 1 by AS, A5, PARTFUN1:def 6;
(((x /. K) '&' (y /. K)) 'or' ((x /. K) '&' ((carry (x,y)) /. K))) 'or' ((y /. K) '&' ((carry (x,y)) /. K)) = 1 by A6, A7;
then add_ovfl (x,y) = 1 by BINARITH:def 6;
hence not x,y are_summable by BINARITH:def 7; :: thesis: verum