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
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
let f be FinSequence of D; :: thesis: ( p in rng f implies ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) )
assume A1: p in rng f ; :: thesis: ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i )
then reconsider i = (p .. f) - 1 as Element of NAT by FINSEQ_4:21, INT_1:5;
A2: p .. f in dom f by A1, FINSEQ_4:20;
take i ; :: thesis: ( i + 1 = p .. f & f :- p = f /^ i )
thus A3: i + 1 = p .. f ; :: thesis: f :- p = f /^ i
thus f :- p = <*(f /. (p .. f))*> ^ (f /^ (p .. f)) by A1, Th38
.= f /^ i by A3, A2, Th31 ; :: thesis: verum