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

end;

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 A8: l in Seg n ; :: thesis: (carry x,y) . l = (0* n) . l
A9: ( 1 <= l & l <= n ) by A8, FINSEQ_1:3;
A10: (0* n) . l = 0 by A8, FUNCOP_1:13;

per cases ( l = 1 or ( 1 + 1 <= l & l <= n ) ) by A9, Th4;

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

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

end;

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

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

end;

end;

end;

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