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 A1: ( x = 0* n & 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 A2: k in Seg n ; :: thesis: (x + y) . k = (0* n) . k
reconsider k = k as Nat ;
A3: (0* n) . k = FALSE by A2, FUNCOP_1:13;
( len x = n & len y = n & len (carry x,y) = n & len (x + y) = n ) by FINSEQ_1:def 18;
then A4: ( 1 <= k & k <= len x & k <= len (carry x,y) & k <= len (x + y) ) by A2, FINSEQ_1:3;
then A5: y /. k = FALSE by A1, A3, FINSEQ_4:24;
A6: (carry x,y) /. k = (carry x,y) . k by A4, FINSEQ_4:24
.= FALSE by A1, A3, Th5 ;
(x + y) . k = (x + y) /. k by A4, FINSEQ_4:24
.= FALSE 'xor' FALSE by A1, A2, A5, A6, BINARITH:def 8
.= FALSE ;
hence (x + y) . k = (0* n) . k by A2, FUNCOP_1:13; :: thesis: verum

end;

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