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 CARD_1:def 7;
then A2: dom ((n + 1) -BinarySequence i) = Seg (n + 1) by FINSEQ_1:def 3;
A3: len (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) = 1 + (len (n -BinarySequence (i div 2))) by FINSEQ_5:8
.= n + 1 by CARD_1:def 7 ;

now :: thesis: for j being Nat st j in dom ((n + 1) -BinarySequence i) holds
((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j

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 )
reconsider z = j as Nat ;
assume A4: j in dom ((n + 1) -BinarySequence i) ; :: thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j
then A5: 1 <= j by A2, FINSEQ_1:1;
A6: j <= n + 1 by A2, A4, FINSEQ_1:1;
A7: len <*(i mod 2)*> = 1 by FINSEQ_1:39;

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

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

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

A9: 2 to_power (((j -' 1) -' 1) + 1) = (2 to_power ((j -' 1) -' 1)) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power ((j -' 1) -' 1)) by POWER:25 ;
j - 1 > 1 - 1 by A8, XREAL_1:9;
then j -' 1 > 0 by A5, XREAL_1:233;
then A10: j -' 1 >= 0 + 1 by NAT_1:13;
then A11: i div (2 to_power (j -' 1)) = i div (2 to_power (((j -' 1) -' 1) + 1)) by XREAL_1:235
.= (i div 2) div (2 to_power ((j -' 1) -' 1)) by A9, NAT_2:27 ;
j - 1 <= n by A6, XREAL_1:20;
then A12: j -' 1 <= n by A5, XREAL_1:233;
then A13: j -' 1 <= len (n -BinarySequence (i div 2)) by CARD_1:def 7;
A14: j -' 1 in Seg n by A10, A12, FINSEQ_1:1;
j <= len ((n + 1) -BinarySequence i) by A6, CARD_1:def 7;
hence ((n + 1) -BinarySequence i) . j = ((n + 1) -BinarySequence i) /. z by A5, FINSEQ_4:15
.= IFEQ (((i div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A2, A4, Def1
.= (n -BinarySequence (i div 2)) /. (j -' 1) by A14, A11, Def1
.= (n -BinarySequence (i div 2)) . (j -' 1) by A10, A13, FINSEQ_4:15
.= (n -BinarySequence (i div 2)) . (j - 1) by A5, XREAL_1:233
.= (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j by A3, A6, A7, A8, FINSEQ_1:24 ;
:: thesis: verum

end;

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

A16: now :: thesis: IFEQ ((i mod 2),0,FALSE,TRUE) = i mod 2

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 A17: 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 A17, NAT_D:12 ;
:: thesis: verum

end;

end;

end;

A18: 2 to_power 0 = 1 by POWER:24;
thus ((n + 1) -BinarySequence i) . j = ((n + 1) -BinarySequence i) /. z by A1, A5, A6, FINSEQ_4:15
.= IFEQ (((i div (2 to_power (1 -' 1))) mod 2),0,FALSE,TRUE) by A2, A4, A15, Def1
.= IFEQ (((i div 1) mod 2),0,FALSE,TRUE) by A18, XREAL_1:232
.= IFEQ ((i mod 2),0,FALSE,TRUE) by NAT_2:4
.= (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j by A15, A16, FINSEQ_1:41 ; :: 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, A3, FINSEQ_2:9; :: thesis: verum