let f be FinSequence; :: thesis: for i being Nat holds rng (f | i) c= rng f
let i be Nat; :: thesis: rng (f | i) c= rng f
f | i c= f by RELAT_1:59;
hence rng (f | i) c= rng f by RELAT_1:11; :: thesis: verum