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

now

let i be Nat; :: thesis: ( i in Seg (n + 1) implies ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE *>) . i )
assume A2: i in Seg (n + 1) ; :: thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE *>) . i
then i in Seg (len ((n + 1) -BinarySequence k)) by FINSEQ_1:def 18;
then A3: i in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def 3;

now

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

suppose A4: i in Seg n ; :: thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE *>) . i

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

end;

suppose A6: i = n + 1 ; :: thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE *>) . i

hence ((n + 1) -BinarySequence k) . i = FALSE by A1, Th27
.= ((n -BinarySequence k) ^ <*FALSE *>) . i by A6, FINSEQ_2:136 ;
:: thesis: verum

end;

end;

end;

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

end;

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