theorem Th20: :: BINARITH:20

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