let p be FinSequence; :: thesis:
let x be object ; :: thesis:
set q1 = p -| x;
set q2 = p |-- x;
set r = (p -| x) ^ <*x*>;
assume A1: x in rng p ; :: thesis:

let k be Nat; :: thesis:
assume k in dom (p |-- x) ; :: thesis:
then (p |-- x) . k = p . ((((x .. p) - 1) + 1) + k) by A1, Def6
.= p . (((len (p -| x)) + 1) + k) by A1, Th34
.= p . (((len (p -| x)) + (len <*x*>)) + k) by FINSEQ_1:40
.= p . ((len ((p -| x) ^ <*x*>)) + k) by FINSEQ_1:22 ;
hence p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k ; :: thesis:

end;

hence ((p -| x) ^ <*x*>) . k = (p -| x) . k by FINSEQ_1:def 7
.= p . k by A1, A5, Th36 ;
:: thesis:

end;

then consider n being Nat such that
A6: n in dom <*x*> and
A7: k = (len (p -| x)) + n ;
n in {1} by A6, FINSEQ_1:2, FINSEQ_1:def 8;
then A8: n = 1 by TARSKI:def 1;
hence ((p -| x) ^ <*x*>) . k = <*x*> . 1 by A6, A7, FINSEQ_1:def 7
.= x by FINSEQ_1:def 8
.= p . (((x .. p) - 1) + 1) by A1, Th19
.= p . k by A1, A7, A8, Th34 ;
:: thesis:

end;

hence p . k = ((p -| x) ^ <*x*>) . k ; :: thesis:

end;