let n be non empty Nat; :: thesis: for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
(n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>
let k be Nat; :: thesis: ( 2 to_power n <= k & k < 2 to_power (n + 1) implies (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *> )
assume that
A1: 2 to_power n <= k and
A2: k < 2 to_power (n + 1) ; :: thesis: (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>

now

let i be Nat; :: thesis: ( i in Seg (n + 1) implies ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>) . i )
reconsider z = i as Nat ;
assume A3: i in Seg (n + 1) ; :: thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>) . i
then i in Seg (len ((n + 1) -BinarySequence k)) by FINSEQ_1:def 18;
then A4: i in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def 3;

now

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

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

then A6: 1 <= i by FINSEQ_1:3;
A7: 2 * (2 to_power (i -' 1)) = (2 to_power (i -' 1)) * (2 to_power 1) by POWER:30
.= 2 to_power ((i -' 1) + 1) by POWER:32
.= 2 to_power ((i - 1) + 1) by A6, XREAL_1:235
.= 2 to_power i ;
2 to_power (i -' 1) > 0 by POWER:39;
then A8: 0 + 1 <= 2 to_power (i -' 1) by NAT_1:13;
i <= n by A5, FINSEQ_1:3;
then A9: 2 * (2 to_power (z -' 1)) divides 2 to_power n by A7, NAT_2:13;

A10: now

per cases ( k div (2 to_power (i -' 1)) is even or not k div (2 to_power (i -' 1)) is even ) ;

suppose A11: k div (2 to_power (i -' 1)) is even ; :: thesis: (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2

then A12: (k div (2 to_power (i -' 1))) mod 2 = 0 by NAT_2:23;
(k -' (2 to_power n)) div (2 to_power (i -' 1)) is even by A1, A8, A9, A11, NAT_2:25;
hence (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2 by A12, NAT_2:23; :: thesis: verum

end;

suppose A13: not k div (2 to_power (i -' 1)) is even ; :: thesis: (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2

then A14: (k div (2 to_power (i -' 1))) mod 2 = 1 by NAT_2:24;
not (k -' (2 to_power n)) div (2 to_power (i -' 1)) is even by A1, A8, A9, A13, NAT_2:25;
hence (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2 by A14, NAT_2:24; :: thesis: verum

end;

end;

end;

i in Seg (len (n -BinarySequence (k -' (2 to_power n)))) by A5, FINSEQ_1:def 18;
then A15: i in dom (n -BinarySequence (k -' (2 to_power n))) by FINSEQ_1:def 3;
thus ((n + 1) -BinarySequence k) . i = ((n + 1) -BinarySequence k) /. i by A4, PARTFUN1:def 8
.= IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A3, Def1
.= (n -BinarySequence (k -' (2 to_power n))) /. i by A5, A10, Def1
.= (n -BinarySequence (k -' (2 to_power n))) . i by A15, PARTFUN1:def 8
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>) . i by A15, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

hence ((n + 1) -BinarySequence k) . i = TRUE by A1, A2, Lm2
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>) . i by A16, FINSEQ_2:136 ;
:: thesis: verum

end;

end;

end;

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

end;

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