let D be non empty set ; :: thesis: for f being FinSequence of D
for p, q being Element of D st p in rng f & q in rng f & p .. f <= q .. f holds
p .. (f -: q) = p .. f
let f be FinSequence of D; :: thesis: for p, q being Element of D st p in rng f & q in rng f & p .. f <= q .. f holds
p .. (f -: q) = p .. f
let p, q be Element of D; :: thesis: ( p in rng f & q in rng f & p .. f <= q .. f implies p .. (f -: q) = p .. f )
A1: f -: q = f | (q .. f) by FINSEQ_5:def 1;
assume ( p in rng f & q in rng f & p .. f <= q .. f ) ; :: thesis: p .. (f -: q) = p .. f
then p in rng (f | (q .. f)) by A1, FINSEQ_5:46;
hence p .. (f -: q) = p .. f by A1, FINSEQ_5:40; :: thesis: verum