theorem Th21: :: BINARI_3:21

for n being non zero Nat
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