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
len (f -: p) = p .. f
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
len (f -: p) = p .. f
let f be FinSequence of D; :: thesis: ( p in rng f implies len (f -: p) = p .. f )
assume p in rng f ; :: thesis: len (f -: p) = p .. f
then p .. f in dom f by FINSEQ_4:20;
then p .. f <= len f by FINSEQ_3:25;
hence len (f -: p) = p .. f by FINSEQ_1:59; :: thesis: verum