theorem Th22: :: BINARI_3:22

for n being non zero Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)