let K be Nat; :: thesis: for x being Element of BOOLEAN * st len x <= K holds
ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*>
let x be Element of BOOLEAN * ; :: thesis: ( len x <= K implies ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*> )
assume AS: len x <= K ; :: thesis: ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*>
A1: K + 0 <= K + 1 by XREAL_1:7;
then AA1: len x <= K + 1 by AS, XXREAL_0:2;
A2: ExtBit (x,K) = x ^ (0* (K -' (len x))) by AS, Def20;
A3: ExtBit (x,(K + 1)) = x ^ (0* ((K + 1) -' (len x))) by A1, Def20, AS, XXREAL_0:2;
B1: K -' (len x) = K - (len x) by XREAL_0:def 2, AS, XREAL_1:48;
(K + 1) -' (len x) = (K + 1) - (len x) by XREAL_0:def 2, AA1, XREAL_1:48;
then (K + 1) -' (len x) = (K -' (len x)) + 1 by B1;
then 0* ((K + 1) -' (len x)) = (0* (K -' (len x))) ^ <*0*> by FINSEQ_2:60;
hence ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*> by A2, FINSEQ_1:32, A3; :: thesis: verum