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

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

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

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

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

end;

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

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

end;

end;

end;

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