theorem :: BINARI_2:16

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