let n be non zero 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 :: thesis: for i being Nat st i in Seg (n + 1) holds
((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i

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 CARD_1:def 7;
then A4: i in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def 3;

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

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

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:1;
A7: 2 * (2 to_power (i -' 1)) = (2 to_power (i -' 1)) * (2 to_power 1) by POWER:25
.= 2 to_power ((i -' 1) + 1) by POWER:27
.= 2 to_power ((i - 1) + 1) by A6, XREAL_1:233
.= 2 to_power i ;
2 to_power (i -' 1) > 0 by POWER:34;
then A8: 0 + 1 <= 2 to_power (i -' 1) by NAT_1:13;
i <= n by A5, FINSEQ_1:1;
then A9: 2 * (2 to_power (z -' 1)) divides 2 to_power n by A7, NAT_2:11;

A10: now :: thesis: (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2

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

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:21;
(k -' (2 to_power n)) div (2 to_power (i -' 1)) is even by A1, A8, A9, A11, NAT_2:23;
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:21; :: thesis: verum

end;

suppose A13: k div (2 to_power (i -' 1)) is odd ; :: 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:22;
(k -' (2 to_power n)) div (2 to_power (i -' 1)) is odd by A1, A8, A9, A13, NAT_2:23;
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:22; :: thesis: verum

end;

end;

end;

i in Seg (len (n -BinarySequence (k -' (2 to_power n)))) by A5, CARD_1:def 7;
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 6
.= 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 6
.= ((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:116 ;
:: 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:119; :: thesis: verum