let x be Element of BOOLEAN * ; :: thesis: for K being Nat st len x <> 0 & len x <= K holds
ExAbsval x = Absval (ExtBit (x,K))
let K be Nat; :: thesis: ( len x <> 0 & len x <= K implies ExAbsval x = Absval (ExtBit (x,K)) )
assume AS: ( len x <> 0 & len x <= K ) ; :: thesis: ExAbsval x = Absval (ExtBit (x,K))
then reconsider n = len x as non zero Nat ;
reconsider y = x as Tuple of n, BOOLEAN by CARD_1:def 7;
ExtBit (x,K) = y ^ (0* (K -' (len x))) by AS, Def20;
then Absval (ExtBit (x,K)) = Absval y by LM080
.= ExAbsval x by Def100 ;
hence ExAbsval x = Absval (ExtBit (x,K)) ; :: thesis: verum