let n, i be Nat; :: thesis: (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2))
A1: len ((n + 1) -BinarySequence i) = n + 1 by FINSEQ_1:def 18;
A2: len (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) = 1 + (len (n -BinarySequence (i div 2))) by FINSEQ_5:8
.= n + 1 by FINSEQ_1:def 18 ;
X: dom ((n + 1) -BinarySequence i) = Seg (n + 1) by A1, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom ((n + 1) -BinarySequence i) implies ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j )
assume A3: j in dom ((n + 1) -BinarySequence i) ; :: thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j
then A4: ( 1 <= j & j <= n + 1 ) by X, FINSEQ_1:3;
A5: len <*(i mod 2)*> = 1 by FINSEQ_1:56;
reconsider z = j as Nat ;

now

per cases ( j > 1 or j = 1 ) by A4, XXREAL_0:1;

suppose A6: j > 1 ; :: thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j

then j - 1 > 1 - 1 by XREAL_1:11;
then j -' 1 > 0 by A4, XREAL_1:235;
then A7: j -' 1 >= 0 + 1 by NAT_1:13;
j - 1 <= n by A4, XREAL_1:22;
then A8: j -' 1 <= n by A4, XREAL_1:235;
then A9: j -' 1 <= len (n -BinarySequence (i div 2)) by FINSEQ_1:def 18;
A10: j -' 1 in Seg n by A7, A8, FINSEQ_1:3;
A11: 2 to_power (((j -' 1) -' 1) + 1) = (2 to_power ((j -' 1) -' 1)) * (2 to_power 1) by POWER:32
.= 2 * (2 to_power ((j -' 1) -' 1)) by POWER:30 ;
A12: i div (2 to_power (j -' 1)) = i div (2 to_power (((j -' 1) -' 1) + 1)) by A7, XREAL_1:237
.= (i div 2) div (2 to_power ((j -' 1) -' 1)) by A11, NAT_2:29 ;
j <= len ((n + 1) -BinarySequence i) by A4, FINSEQ_1:def 18;
hence ((n + 1) -BinarySequence i) . j = ((n + 1) -BinarySequence i) /. z by A4, FINSEQ_4:24
.= IFEQ ((i div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A3, Def1, X
.= (n -BinarySequence (i div 2)) /. (j -' 1) by A10, A12, Def1
.= (n -BinarySequence (i div 2)) . (j -' 1) by A7, A9, FINSEQ_4:24
.= (n -BinarySequence (i div 2)) . (j - 1) by A4, XREAL_1:235
.= (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j by A2, A4, A5, A6, FINSEQ_1:37 ;
:: thesis: verum

end;

suppose A13: j = 1 ; :: thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j

A14: 2 to_power 0 = 1 by POWER:29;

A15: now

per cases ( i mod 2 = 0 or i mod 2 <> 0 ) ;

suppose i mod 2 = 0 ; :: thesis: IFEQ (i mod 2),0 ,FALSE ,TRUE = i mod 2

hence IFEQ (i mod 2),0 ,FALSE ,TRUE = i mod 2 by FUNCOP_1:def 8; :: thesis: verum

end;

suppose A16: i mod 2 <> 0 ; :: thesis: IFEQ (i mod 2),0 ,FALSE ,TRUE = i mod 2

hence IFEQ (i mod 2),0 ,FALSE ,TRUE = 1 by FUNCOP_1:def 8
.= i mod 2 by A16, NAT_D:12 ;
:: thesis: verum

end;

end;

end;

thus ((n + 1) -BinarySequence i) . j = ((n + 1) -BinarySequence i) /. z by A1, A4, FINSEQ_4:24
.= IFEQ ((i div (2 to_power (1 -' 1))) mod 2),0 ,FALSE ,TRUE by A3, A13, Def1, X
.= IFEQ ((i div 1) mod 2),0 ,FALSE ,TRUE by A14, XREAL_1:234
.= IFEQ (i mod 2),0 ,FALSE ,TRUE by NAT_2:6
.= (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j by A13, A15, FINSEQ_1:58 ; :: thesis: verum

end;

end;

end;

hence ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j ; :: thesis: verum

end;

hence (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2)) by A1, A2, FINSEQ_2:10; :: thesis: verum