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 i in Seg (len 0n) by FINSEQ_1:def 18;
then A4: i in dom 0n by FINSEQ_1:def 3;
A5: i >= 1 by A3, FINSEQ_1:3;
i <= n + 1 by A2, FINSEQ_1:3;
then i - 1 <= (n + 1) - 1 by XREAL_1:11;
then A6: i -' 1 <= (n + 1) - 1 by A5, XREAL_1:235;
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 A5, XREAL_1:235;
then n -' (i -' 1) > 0 by A6, XREAL_1:235;
then consider n1 being Nat such that
A7: n -' (i -' 1) = n1 + 1 by NAT_1:6;
reconsider n1 = n1 as Nat ;
A8: 2 to_power (n -' (i -' 1)) = (2 to_power n1) * (2 to_power 1) by A7, POWER:32
.= (2 to_power n1) * 2 by POWER:30 ;
A9: 2 to_power (i -' 1) > 0 by POWER:39;
n = (n - (i -' 1)) + (i -' 1)
.= (n -' (i -' 1)) + (i -' 1) by A6, XREAL_1:235 ;
then 2 to_power n = (2 to_power (n -' (i -' 1))) * (2 to_power (i -' 1)) by POWER:32;
then A10: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = (2 to_power (n -' (i -' 1))) mod 2 by A9, NAT_D:20
.= 0 by A8, 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 A4, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

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 A12: n + 1 in dom ((n + 1) -BinarySequence (2 to_power n)) by FINSEQ_1:def 3;
A13: 2 to_power n > 0 by POWER:39;
i -' 1 = (n + 1) - 1 by A11, NAT_D:37
.= n ;
then A14: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = 1 mod 2 by A13, NAT_2:5
.= 1 by NAT_D:14 ;
thus ((n + 1) -BinarySequence (2 to_power n)) . i = ((n + 1) -BinarySequence (2 to_power n)) /. i by A11, A12, PARTFUN1:def 8
.= IFEQ (((2 to_power n) div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A2, Def1
.= TRUE by A14, 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