let n, k be Nat; :: thesis: ( k < 2 to_power n implies ((n + 1) -BinarySequence k) . (n + 1) = FALSE )
assume A1: k < 2 to_power n ; :: thesis: ((n + 1) -BinarySequence k) . (n + 1) = FALSE
(n + 1) -' 1 = (n + 1) - 1 by NAT_D:37
.= n ;
then A2: (k div (2 to_power ((n + 1) -' 1))) mod 2 = 0 mod 2 by A1, NAT_D:27
.= 0 by NAT_D:26 ;
A3: n + 1 in Seg (n + 1) by FINSEQ_1:6;
then n + 1 in Seg (len ((n + 1) -BinarySequence k)) by FINSEQ_1:def 18;
then n + 1 in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def 3;
hence ((n + 1) -BinarySequence k) . (n + 1) = ((n + 1) -BinarySequence k) /. (n + 1) by PARTFUN1:def 8
.= IFEQ ((k div (2 to_power ((n + 1) -' 1))) mod 2),0 ,FALSE ,TRUE by A3, Def1
.= FALSE by A2, FUNCOP_1:def 8 ;
:: thesis: verum