let p be FinSequence; :: thesis: for A being set holds rng (p - A) c= rng p
let A be set ; :: thesis: rng (p - A) c= rng p
rng (p - A) = (rng p) \ A by Th63;
hence rng (p - A) c= rng p ; :: thesis: verum