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 = 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 ;
A5: 1 <= k by A3, FINSEQ_1:1;
len x = n by CARD_1:def 7;
then k <= len x by A3, FINSEQ_1:1;
then A6: y /. k = FALSE by A1, A2, A4, A5, FINSEQ_4:15;
len (carry (x,y)) = n by CARD_1:def 7;
then k <= len (carry (x,y)) by A3, FINSEQ_1:1;
then A7: (carry (x,y)) /. k = (carry (x,y)) . k by A5, FINSEQ_4:15
.= FALSE by A1, A2, A4, Th5 ;
len (x + y) = n by CARD_1:def 7;
then k <= len (x + y) by A3, FINSEQ_1:1;
then (x + y) . k = (x + y) /. k by A5, FINSEQ_4:15
.= FALSE 'xor' FALSE by A1, A2, A3, A6, A7, BINARITH:def 5
.= FALSE ;
hence (x + y) . k = (0* n) . k ; :: thesis: verum

end;

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