let i be natural number ; :: thesis: for p being FinSequence holds rng (Del p,i) c= rng p
let p be FinSequence; :: thesis: rng (Del p,i) c= rng p
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Del p,i) or x in rng p )
assume x in rng (Del p,i) ; :: thesis: x in rng p
hence x in rng p by FUNCT_1:25; :: thesis: verum