let n be non empty Nat; :: thesis: for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
x,y are_summable
let x, y be Tuple of n, BOOLEAN ; :: thesis: ( x = 0* n & y = 0* n implies x,y are_summable )
assume that
A1: x = 0* n and
A2: y = 0* n ; :: thesis: x,y are_summable
A3: 1 <= n by NAT_1:14;
then A4: n in Seg n by FINSEQ_1:3;
len x = n by FINSEQ_1:def 18;
then x /. n = (0* n) . n by A1, A3, FINSEQ_4:24
.= FALSE by A4, FUNCOP_1:13 ;
then add_ovfl x,y = ((FALSE '&' FALSE ) 'or' (FALSE '&' ((carry x,y) /. n))) 'or' (FALSE '&' ((carry x,y) /. n)) by A1, A2, BINARITH:def 9
.= FALSE ;
hence x,y are_summable by BINARITH:def 10; :: thesis: verum