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