let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
f |-- p = f /^ (p .. f)
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
f |-- p = f /^ (p .. f)
let f be FinSequence of D; :: thesis: ( p in rng f implies f |-- p = f /^ (p .. f) )
assume A1: p in rng f ; :: thesis: f |-- p = f /^ (p .. f)
then A2: len (f |-- p) = (len f) - (p .. f) by FINSEQ_4:def 6;
A3: p .. f <= len f by A1, FINSEQ_4:21;
then A4: len (f /^ (p .. f)) = (len f) - (p .. f) by RFINSEQ:def 1;
A5: ( Seg (len (f |-- p)) = dom (f |-- p) & Seg (len (f /^ (p .. f))) = dom (f /^ (p .. f)) ) by FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom (f |-- p) holds
(f |-- p) . i = (f /^ (p .. f)) . i

let i be Nat; :: thesis: ( i in dom (f |-- p) implies (f |-- p) . i = (f /^ (p .. f)) . i )
assume A6: i in dom (f |-- p) ; :: thesis: (f |-- p) . i = (f /^ (p .. f)) . i
hence (f |-- p) . i = f . (i + (p .. f)) by A1, FINSEQ_4:def 6
.= (f /^ (p .. f)) . i by A2, A3, A4, A5, A6, RFINSEQ:def 1 ;
:: thesis: verum

end;

hence f |-- p = f /^ (p .. f) by A2, A4, FINSEQ_2:9; :: thesis: verum