let n be non empty Nat; :: thesis: for x being Tuple of n, BOOLEAN st x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE holds
carry x,(Bin1 n) = 'not' (Bin1 n)
let x be Tuple of n, BOOLEAN ; :: thesis: ( x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE implies carry x,(Bin1 n) = 'not' (Bin1 n) )
assume that
A1: x /. n = TRUE and
A2: (carry x,(Bin1 n)) /. n = TRUE ; :: thesis: carry x,(Bin1 n) = 'not' (Bin1 n)

now

A3: len ('not' (Bin1 n)) = n by FINSEQ_1:def 18;
let i be Nat; :: thesis: ( i in Seg n implies (carry x,(Bin1 n)) . b₁ = ('not' (Bin1 n)) . b₁ )
reconsider z = i as Nat ;
A4: len (carry x,(Bin1 n)) = n by FINSEQ_1:def 18;
assume A5: i in Seg n ; :: thesis: (carry x,(Bin1 n)) . b₁ = ('not' (Bin1 n)) . b₁
then A6: 1 <= i by FINSEQ_1:3;
A7: i <= n by A5, FINSEQ_1:3;

per cases ( i = 1 or i <> 1 ) ;

suppose A8: i = 1 ; :: thesis: (carry x,(Bin1 n)) . b₁ = ('not' (Bin1 n)) . b₁

thus (carry x,(Bin1 n)) . i = (carry x,(Bin1 n)) /. z by A6, A7, A4, FINSEQ_4:24
.= 'not' TRUE by A8, BINARITH:def 5
.= 'not' ((Bin1 n) /. i) by A5, A8, BINARI_2:7
.= ('not' (Bin1 n)) /. z by A5, BINARITH:def 4
.= ('not' (Bin1 n)) . i by A6, A7, A3, FINSEQ_4:24 ; :: thesis: verum

end;

suppose A9: i <> 1 ; :: thesis: (carry x,(Bin1 n)) . b₁ = ('not' (Bin1 n)) . b₁

A10: not i is empty by A5, FINSEQ_1:3;
thus (carry x,(Bin1 n)) . i = (carry x,(Bin1 n)) /. z by A6, A7, A4, FINSEQ_4:24
.= 'not' FALSE by A1, A2, A7, A9, A10, Th20
.= 'not' ((Bin1 n) /. i) by A5, A9, BINARI_2:8
.= ('not' (Bin1 n)) /. z by A5, BINARITH:def 4
.= ('not' (Bin1 n)) . i by A6, A7, A3, FINSEQ_4:24 ; :: thesis: verum

end;

end;

end;

hence carry x,(Bin1 n) = 'not' (Bin1 n) by FINSEQ_2:139; :: thesis: verum