let n be non empty 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:18;
k + 1 = j ;
then A6: ( 1 <= k & k < n ) by A4, A5, NAT_1:13;
then A7: k in Seg n by FINSEQ_1:3;
len (0* n) = n by FINSEQ_1:def 18;
then A8: x /. k = (0* n) . k by A1, A6, FINSEQ_4:24
.= FALSE by A7, FUNCOP_1:13 ;
A9: j = k + 1 ;
len (carry x,y) = n by FINSEQ_1:def 18;
then (carry x,y) . j = (carry x,y) /. j by A4, A5, FINSEQ_4:24
.= ((FALSE '&' FALSE ) 'or' (FALSE '&' ((carry x,y) /. k))) 'or' (FALSE '&' ((carry x,y) /. k)) by A1, A2, A6, A9, A8, BINARITH:def 5
.= FALSE ;
hence (carry x,y) . j = 0 ; :: thesis: verum

end;

len (carry x,y) = n by FINSEQ_1:def 18;
then 1 <= len (carry x,y) by NAT_1:14;
then A10: (carry x,y) . 1 = (carry x,y) /. 1 by FINSEQ_4:24
.= 0 by BINARITH:def 5 ;
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 A11: l in Seg n ; :: thesis: (carry x,y) . l = (0* n) . l
A12: 1 <= l by A11, FINSEQ_1:3;
A13: (0* n) . l = 0 by A11, FUNCOP_1:13;

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

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

hence (carry x,y) . l = (0* n) . l by A10, A11, FUNCOP_1:13; :: thesis: verum

end;

suppose A14: ( 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, A13, A14; :: thesis: verum

end;

end;

end;

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