for x being Element of BOOLEAN *
for K being Nat st len x <> 0 & len x <= K holds
ExAbsval x = Absval (ExtBit (x,K))