let K be non zero Nat; :: thesis: for x being Element of BOOLEAN * st len x = K holds
ExtBit (x,K) = x
let x be Element of BOOLEAN * ; :: thesis: ( len x = K implies ExtBit (x,K) = x )
assume PA1: len x = K ; :: thesis: ExtBit (x,K) = x
then A1: K - (len x) = 0 ;
thus ExtBit (x,K) = x ^ (0* (K -' (len x))) by PA1, Def20
.= x ^ (0* 0) by XREAL_0:def 2, A1
.= x by FINSEQ_1:34 ; :: thesis: verum