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