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 = 0* n
let x, y be Tuple of n, BOOLEAN ; :: thesis: ( x = 0* n & y = 0* n implies x + y = 0* n )
assume that
A1: x = 0* n and
A2: y = 0* n ; :: thesis: x + y = 0* n
for k being Nat st k in Seg n holds
(x + y) . k = (0* n) . k

proof

let k be Nat; :: thesis: ( k in Seg n implies (x + y) . k = (0* n) . k )
assume A3: k in Seg n ; :: thesis: (x + y) . k = (0* n) . k
reconsider k = k as Nat ;
A4: (0* n) . k = FALSE by A3, FUNCOP_1:13;
A5: 1 <= k by A3, FINSEQ_1:3;
len x = n by FINSEQ_1:def 18;
then k <= len x by A3, FINSEQ_1:3;
then A6: y /. k = FALSE by A1, A2, A4, A5, FINSEQ_4:24;
len (carry x,y) = n by FINSEQ_1:def 18;
then k <= len (carry x,y) by A3, FINSEQ_1:3;
then A7: (carry x,y) /. k = (carry x,y) . k by A5, FINSEQ_4:24
.= FALSE by A1, A2, A4, Th5 ;
len (x + y) = n by FINSEQ_1:def 18;
then k <= len (x + y) by A3, FINSEQ_1:3;
then (x + y) . k = (x + y) /. k by A5, FINSEQ_4:24
.= FALSE 'xor' FALSE by A1, A2, A3, A6, A7, BINARITH:def 8
.= FALSE ;
hence (x + y) . k = (0* n) . k by A3, FUNCOP_1:13; :: thesis: verum

end;

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