let n be non zero Nat; :: thesis: for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
carry (x,y) = 0* n
let x, y be Tuple of n, BOOLEAN ; :: thesis: ( x = 0* n & y = 0* n implies carry (x,y) = 0* n )
assume that
A1: x = 0* n and
A2: y = 0* n ; :: thesis: carry (x,y) = 0* n
A3: for j being Nat st 1 < j & j <= n holds
(carry (x,y)) . j = 0

proof

let j be Nat; :: thesis: ( 1 < j & j <= n implies (carry (x,y)) . j = 0 )
assume that
A4: 1 < j and
A5: j <= n ; :: thesis: (carry (x,y)) . j = 0
reconsider k = j - 1 as Element of NAT by A4, INT_1:5;
k + 1 = j ;
then A6: ( 1 <= k & k < n ) by A4, A5, NAT_1:13;
len (0* n) = n by CARD_1:def 7;
then A7: x /. k = (0* n) . k by A1, A6, FINSEQ_4:15
.= FALSE ;
A8: j = k + 1 ;
len (carry (x,y)) = n by CARD_1:def 7;
then (carry (x,y)) . j = (carry (x,y)) /. j by A4, A5, FINSEQ_4:15
.= ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (x,y)) /. k))) 'or' (FALSE '&' ((carry (x,y)) /. k)) by A1, A2, A6, A8, A7, BINARITH:def 2
.= FALSE ;
hence (carry (x,y)) . j = 0 ; :: thesis: verum

end;

1 <= len (carry (x,y)) by NAT_1:14;
then A9: (carry (x,y)) . 1 = (carry (x,y)) /. 1 by FINSEQ_4:15
.= 0 by BINARITH:def 2 ;
for l being Nat st l in Seg n holds
(carry (x,y)) . l = (0* n) . l

proof

let l be Nat; :: thesis: ( l in Seg n implies (carry (x,y)) . l = (0* n) . l )
assume A10: l in Seg n ; :: thesis: (carry (x,y)) . l = (0* n) . l
A11: 1 <= l by A10, FINSEQ_1:1;
A12: (0* n) . l = 0 ;

per cases ( l = 1 or ( 1 + 1 <= l & l <= n ) ) by A10, A11, Th4, FINSEQ_1:1;

suppose l = 1 ; :: thesis: (carry (x,y)) . l = (0* n) . l

hence (carry (x,y)) . l = (0* n) . l by A9; :: thesis: verum

end;

suppose A13: ( 1 + 1 <= l & l <= n ) ; :: thesis: (carry (x,y)) . l = (0* n) . l

then 1 < l by NAT_1:13;
hence (carry (x,y)) . l = (0* n) . l by A3, A12, A13; :: thesis: verum

end;

end;

end;

hence carry (x,y) = 0* n by A1, FINSEQ_2:119; :: thesis: verum