let n be non empty Nat; :: thesis: (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE *>
0* n in BOOLEAN * by Th5;
then A1: 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* n) = n by FINSEQ_1:def 18;
then reconsider 0n = 0* n as Tuple of n, BOOLEAN by A1, FINSEQ_2:110;

now

let i be Nat; :: thesis: ( i in Seg (n + 1) implies ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE *>) . i )
assume A2: i in Seg (n + 1) ; :: thesis: ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE *>) . i

now

per cases ( i in Seg n or i = n + 1 ) by A2, FINSEQ_2:8;

suppose A3: i in Seg n ; :: thesis: ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE *>) . i

then A4: i >= 1 by FINSEQ_1:3;
i <= n + 1 by A2, FINSEQ_1:3;
then i - 1 <= (n + 1) - 1 by XREAL_1:11;
then A5: i -' 1 <= (n + 1) - 1 by A4, XREAL_1:235;
n = (n - (i -' 1)) + (i -' 1)
.= (n -' (i -' 1)) + (i -' 1) by A5, XREAL_1:235 ;
then A6: 2 to_power n = (2 to_power (n -' (i -' 1))) * (2 to_power (i -' 1)) by POWER:32;
i in Seg (len 0n) by A3, FINSEQ_1:def 18;
then A7: i in dom 0n by FINSEQ_1:def 3;
n >= i by A3, FINSEQ_1:3;
then n + 1 > i by NAT_1:13;
then n > i - 1 by XREAL_1:21;
then n - (i - 1) > 0 by XREAL_1:52;
then n - (i -' 1) > 0 by A4, XREAL_1:235;
then n -' (i -' 1) > 0 by A5, XREAL_1:235;
then consider n1 being Nat such that
A8: n -' (i -' 1) = n1 + 1 by NAT_1:6;
reconsider n1 = n1 as Nat ;
A9: 2 to_power (n -' (i -' 1)) = (2 to_power n1) * (2 to_power 1) by A8, POWER:32
.= (2 to_power n1) * 2 by POWER:30 ;
2 to_power (i -' 1) > 0 by POWER:39;
then A10: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = (2 to_power (n -' (i -' 1))) mod 2 by A6, NAT_D:20
.= 0 by A9, NAT_D:13 ;
i in Seg (len ((n + 1) -BinarySequence (2 to_power n))) by A2, FINSEQ_1:def 18;
then i in dom ((n + 1) -BinarySequence (2 to_power n)) by FINSEQ_1:def 3;
hence ((n + 1) -BinarySequence (2 to_power n)) . i = ((n + 1) -BinarySequence (2 to_power n)) /. i by PARTFUN1:def 8
.= IFEQ (((2 to_power n) div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A2, Def1
.= 0 by A10, FUNCOP_1:def 8
.= 0n . i by A3, FUNCOP_1:13
.= (0n ^ <*TRUE *>) . i by A7, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A11: i = n + 1 ; :: thesis: ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE *>) . i

A12: 2 to_power n > 0 by POWER:39;
i -' 1 = (n + 1) - 1 by A11, NAT_D:37
.= n ;
then A13: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = 1 mod 2 by A12, NAT_2:5
.= 1 by NAT_D:14 ;
n + 1 in Seg (n + 1) by FINSEQ_1:6;
then n + 1 in Seg (len ((n + 1) -BinarySequence (2 to_power n))) by FINSEQ_1:def 18;
then n + 1 in dom ((n + 1) -BinarySequence (2 to_power n)) by FINSEQ_1:def 3;
hence ((n + 1) -BinarySequence (2 to_power n)) . i = ((n + 1) -BinarySequence (2 to_power n)) /. i by A11, PARTFUN1:def 8
.= IFEQ (((2 to_power n) div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A2, Def1
.= TRUE by A13, FUNCOP_1:def 8
.= (0n ^ <*TRUE *>) . i by A11, FINSEQ_2:136 ;
:: thesis: verum

end;

end;

end;

hence ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE *>) . i ; :: thesis: verum

end;

hence (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE *> by FINSEQ_2:139; :: thesis: verum