let x be Nat; :: thesis: x < 2 to_power (LenBSeq x)

per cases ( x = 0 or x <> 0 ) ;

suppose C1: x = 0 ; :: thesis: x < 2 to_power (LenBSeq x)

then LenBSeq x = 1 by Def1;
hence x < 2 to_power (LenBSeq x) by POWER:25, C1; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: x < 2 to_power (LenBSeq x)

then consider n being Nat such that
C2: ( 2 to_power n <= x & x < 2 to_power (n + 1) & LenBSeq x = n + 1 ) by Def1;
thus x < 2 to_power (LenBSeq x) by C2; :: thesis: verum

end;

end;