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

now :: thesis: for i being Nat st i in Seg (n + 1) holds
((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE*>) . i

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

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

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

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

then A3: i >= 1 by FINSEQ_1:1;
i <= n + 1 by A1, FINSEQ_1:1;
then i - 1 <= (n + 1) - 1 by XREAL_1:9;
then A4: i -' 1 <= (n + 1) - 1 by A3, XREAL_1:233;
n = (n - (i -' 1)) + (i -' 1)
.= (n -' (i -' 1)) + (i -' 1) by A4, XREAL_1:233 ;
then A5: 2 to_power n = (2 to_power (n -' (i -' 1))) * (2 to_power (i -' 1)) by POWER:27;
i in Seg (len 0n) by A2, CARD_1:def 7;
then A6: i in dom 0n by FINSEQ_1:def 3;
n >= i by A2, FINSEQ_1:1;
then n + 1 > i by NAT_1:13;
then n > i - 1 by XREAL_1:19;
then n - (i - 1) > 0 by XREAL_1:50;
then n - (i -' 1) > 0 by A3, XREAL_1:233;
then n -' (i -' 1) > 0 by A4, XREAL_1:233;
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:27
.= (2 to_power n1) * 2 by POWER:25 ;
2 to_power (i -' 1) > 0 by POWER:34;
then A9: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = (2 to_power (n -' (i -' 1))) mod 2 by A5, NAT_D:18
.= 0 by A8, NAT_D:13 ;
i in Seg (len ((n + 1) -BinarySequence (2 to_power n))) by A1, CARD_1:def 7;
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 6
.= IFEQ ((((2 to_power n) div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1
.= 0 by A9, FUNCOP_1:def 8
.= 0n . i by A2, FUNCOP_1:7
.= (0n ^ <*TRUE*>) . i by A6, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

A11: 2 to_power n > 0 by POWER:34;
i -' 1 = (n + 1) - 1 by A10, NAT_D:37
.= n ;
then A12: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = 1 mod 2 by A11, NAT_2:3
.= 1 by NAT_D:14 ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in Seg (len ((n + 1) -BinarySequence (2 to_power n))) by CARD_1:def 7;
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 A10, PARTFUN1:def 6
.= IFEQ ((((2 to_power n) div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1
.= TRUE by A12, FUNCOP_1:def 8
.= (0n ^ <*TRUE*>) . i by A10, FINSEQ_2:116 ;
:: 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:119; :: thesis: verum