let n be non zero 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;
len x = n by CARD_1:def 7;
then x /. n = (0* n) . n by A1, A3, FINSEQ_4:15
.= FALSE ;
then add_ovfl (x,y) = ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (x,y)) /. n))) 'or' (FALSE '&' ((carry (x,y)) /. n)) by A1, A2, BINARITH:def 6
.= FALSE ;
hence x,y are_summable by BINARITH:def 7; :: thesis: verum