let p be FinSequence; :: thesis: for x being object st x in rng p holds
rng (p -| x) c= rng p
let x be object ; :: thesis: ( x in rng p implies rng (p -| x) c= rng p )
assume x in rng p ; :: thesis: rng (p -| x) c= rng p
then ex n being Nat st
( n = (x .. p) - 1 & p | (Seg n) = p -| x ) by Def5;
hence rng (p -| x) c= rng p by RELAT_1:70; :: thesis: verum