let n be non zero Nat; :: thesis: for x, y being Tuple of n, BOOLEAN st y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
x = 'not' y
let x, y be Tuple of n, BOOLEAN ; :: thesis: ( y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE implies x = 'not' y )
assume that
A1: y = 0* n and
A2: x /. n = TRUE and
A3: (carry (x,(Bin1 n))) /. n = TRUE ; :: thesis: x = 'not' y
A4: len x = n by CARD_1:def 7;
A5: len ('not' y) = n by CARD_1:def 7;
A6: len y = n by CARD_1:def 7;
A7: len (carry (x,(Bin1 n))) = n by CARD_1:def 7;

now :: thesis: for i being Nat st i in Seg n holds
x . i = ('not' y) . i

let i be Nat; :: thesis: ( i in Seg n implies x . i = ('not' y) . i )
reconsider z = i as Nat ;
assume A8: i in Seg n ; :: thesis: x . i = ('not' y) . i
then A9: 1 <= i by FINSEQ_1:1;
A10: i <= n by A8, FINSEQ_1:1;
A11: y . i = FALSE by A1, A8, FUNCOP_1:7;

now :: thesis: x . i = ('not' y) . i

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

suppose A12: i = 1 ; :: thesis: x . i = ('not' y) . i

A13: n >= 1 by NAT_1:14;

now :: thesis: x . i = ('not' y) . i

per cases ( n = 1 or n > 1 ) by A13, XXREAL_0:1;

suppose n = 1 ; :: thesis: x . i = ('not' y) . i

hence x . i = ('not' y) . i by A3, BINARITH:def 2; :: thesis: verum

end;

suppose A14: n > 1 ; :: thesis: x . i = ('not' y) . i

A15: len ('not' (Bin1 n)) = n by CARD_1:def 7;
A16: (carry (x,(Bin1 n))) /. i = FALSE by A12, BINARITH:def 2;
then A17: ((Bin1 n) /. i) '&' ((carry (x,(Bin1 n))) /. i) = FALSE ;
A18: 1 + 1 <= n by A14, NAT_1:13;
then A19: 2 in Seg n by FINSEQ_1:1;
(carry (x,(Bin1 n))) . (i + 1) = ('not' (Bin1 n)) . 2 by A2, A3, A12, Th20
.= ('not' (Bin1 n)) /. 2 by A18, A15, FINSEQ_4:15
.= 'not' ((Bin1 n) /. 2) by A19, BINARITH:def 1
.= 'not' FALSE by A19, BINARI_2:6
.= TRUE ;
then A20: TRUE = (carry (x,(Bin1 n))) /. (i + 1) by A7, A12, A18, FINSEQ_4:15
.= ((x /. i) '&' ((Bin1 n) /. i)) 'or' ((x /. i) '&' ((carry (x,(Bin1 n))) /. i)) by A12, A14, A16, A17, BINARITH:def 2
.= (x /. i) '&' ((Bin1 n) /. i) by A16 ;
thus x . i = x /. z by A4, A9, A10, FINSEQ_4:15
.= 'not' FALSE by A20, MARGREL1:12
.= 'not' (y /. z) by A6, A9, A10, A11, FINSEQ_4:15
.= ('not' y) /. z by A8, BINARITH:def 1
.= ('not' y) . i by A5, A9, A10, FINSEQ_4:15 ; :: thesis: verum

end;

end;

end;

hence x . i = ('not' y) . i ; :: thesis: verum

end;

suppose A21: i <> 1 ; :: thesis: x . i = ('not' y) . i

1 <= i by A8, FINSEQ_1:1;
then 0 < i ;
then A22: not i is empty ;
thus x . i = x /. z by A4, A9, A10, FINSEQ_4:15
.= 'not' FALSE by A2, A3, A10, A21, A22, Th19
.= 'not' (y /. z) by A6, A9, A10, A11, FINSEQ_4:15
.= ('not' y) /. z by A8, BINARITH:def 1
.= ('not' y) . i by A5, A9, A10, FINSEQ_4:15 ; :: thesis: verum

end;

end;

end;

hence x . i = ('not' y) . i ; :: thesis: verum

end;

hence x = 'not' y by FINSEQ_2:119; :: thesis: verum