let n, k be Nat; :: thesis: ( k < 2 to_power n implies ((n + 1) -BinarySequence k) . (n + 1) = FALSE )
A1: (n + 1) -' 1 = (n + 1) - 1 by NAT_D:37
.= n ;
assume k < 2 to_power n ; :: thesis: ((n + 1) -BinarySequence k) . (n + 1) = FALSE
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:4;
then n + 1 in Seg (len ((n + 1) -BinarySequence k)) by CARD_1:def 7;
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 6
.= 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