theorem Th14: :: BINARI_2:14

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