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
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
f /. (p .. f) = p
let f be FinSequence of D; :: thesis: ( p in rng f implies f /. (p .. f) = p )
assume p in rng f ; :: thesis: f /. (p .. f) = p
then ( p .. f in dom f & f . (p .. f) = p ) by FINSEQ_4:19, FINSEQ_4:20;
hence f /. (p .. f) = p by PARTFUN1:def 6; :: thesis: verum