theorem Th9: :: BINARI_2:9

for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>