let n be non zero 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 :: thesis: for i being Nat st i in Seg n holds
(carry (x,(Bin1 n))) . i = ('not' (Bin1 n)) . i

A3: len ('not' (Bin1 n)) = n by CARD_1:def 7;
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 CARD_1:def 7;
assume A5: i in Seg n ; :: thesis: (carry (x,(Bin1 n))) . b₁ = ('not' (Bin1 n)) . b₁
then A6: 1 <= i by FINSEQ_1:1;
A7: i <= n by A5, FINSEQ_1:1;

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:15
.= 'not' TRUE by A8, BINARITH:def 2
.= 'not' ((Bin1 n) /. i) by A5, A8, BINARI_2:5
.= ('not' (Bin1 n)) /. z by A5, BINARITH:def 1
.= ('not' (Bin1 n)) . i by A6, A7, A3, FINSEQ_4:15 ; :: thesis: verum

end;

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

1 <= i by A5, FINSEQ_1:1;
then 0 < i ;
then A10: not i is zero ;
thus (carry (x,(Bin1 n))) . i = (carry (x,(Bin1 n))) /. z by A6, A7, A4, FINSEQ_4:15
.= 'not' FALSE by A1, A2, A7, A9, A10, Th19
.= 'not' ((Bin1 n) /. i) by A5, A9, BINARI_2:6
.= ('not' (Bin1 n)) /. z by A5, BINARITH:def 1
.= ('not' (Bin1 n)) . i by A6, A7, A3, FINSEQ_4:15 ; :: thesis: verum

end;

end;

end;

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