let n be non zero Nat; :: thesis:
let x, y be Tuple of n, BOOLEAN ; :: thesis:
assume that
A1: x = 0* n and
A2: y = 0* n ; :: thesis:
for k being Nat st k in Seg n holds
(x + y) . k = (0* n) . k

let k be Nat; :: thesis:
assume A3: k in Seg n ; :: thesis:
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:

end;