theorem Th10: :: BINARI_2:10

for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))