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 ( 1 <= p .. f & p .. f <= p .. f ) by FINSEQ_4:31;
then A2: p .. f in Seg (p .. f) ;
A3: p .. f in dom f by A1, FINSEQ_4:30;
thus (f -: p) /. (p .. f) = f /. (p .. f) by A1, A2, Th46
.= f . (p .. f) by A3, PARTFUN1:def 8
.= p by A1, FINSEQ_4:29 ; :: thesis: verum