let n be Nat; :: thesis: for x being Tuple of n + 1, BOOLEAN st x . (n + 1) = 1 holds
( 2 to_power n <= Absval x & Absval x < 2 to_power (n + 1) )
let x be Tuple of n + 1, BOOLEAN ; :: thesis: ( x . (n + 1) = 1 implies ( 2 to_power n <= Absval x & Absval x < 2 to_power (n + 1) ) )
assume AS: x . (n + 1) = 1 ; :: thesis: ( 2 to_power n <= Absval x & Absval x < 2 to_power (n + 1) )
len x = n + 1 by CARD_1:def 7;
then n + 1 in Seg (len x) by FINSEQ_1:4;
then n + 1 in dom x by FINSEQ_1:def 3;
then P3: x /. (n + 1) = 1 by AS, PARTFUN1:def 6;
0 <= (n + 1) - 1 ;
then (n + 1) -' 1 = n by XREAL_0:def 2;
hence 2 to_power n <= Absval x by BINARI_4:12, P3; :: thesis: Absval x < 2 to_power (n + 1)
thus Absval x < 2 to_power (n + 1) by BINARI_3:1; :: thesis: verum