theorem Th5: :: BINARI_3:5

for n being Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
'not' y = n |-> 1