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 A1: ( x = 0* n & y = 0* n ) ; :: thesis: x,y are_summable
A2: ( 1 <= n & len x = n ) by FINSEQ_1:def 18, NAT_1:14;
then A3: n in Seg n by FINSEQ_1:3;
x /. n = (0* n) . n by A1, A2, FINSEQ_4:24
.= FALSE by A3, FUNCOP_1:13 ;
then add_ovfl x,y = ((FALSE '&' FALSE ) 'or' (FALSE '&' ((carry x,y) /. n))) 'or' (FALSE '&' ((carry x,y) /. n)) by A1, BINARITH:def 9
.= FALSE ;
hence x,y are_summable by BINARITH:def 10; :: thesis: verum