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 CARD_1:def 7;
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:7;

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 CARD_1:def 7;
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 6
.= 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 6
.= ((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:116 ;
:: 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:119; :: thesis: verum