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:14; :: thesis: verum