let f be XFinSequence; :: thesis: for n being Nat holds rng (f /^ n) c= rng f
let n be Nat; :: thesis: rng (f /^ n) c= rng f
thus rng (f /^ n) c= rng f :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (f /^ n) or z in rng f )
assume z in rng (f /^ n) ; :: thesis: z in rng f
then consider x being set such that
B1: ( x in dom (f /^ n) & z = (f /^ n) . x ) by FUNCT_1:def 5;
reconsider nx = x as Element of NAT by B1;
nx < len (f /^ n) by B1, NAT_1:45;
then B3: nx < (len f) -' n by Def2;

per cases ( n < len f or n >= len f ) ;

suppose C0: n < len f ; :: thesis: z in rng f

C1: (f /^ n) . nx = f . (nx + n) by Def2, B1;
(len f) -' n = (len f) - n by C0, XREAL_1:235;
then nx + n < len f by B3, XREAL_1:22;
then nx + n in dom f by NAT_1:45;
hence z in rng f by C1, B1, FUNCT_1:def 5; :: thesis: verum

end;

suppose n >= len f ; :: thesis: z in rng f

then f /^ n = {} by TH80e;
hence z in rng f by B1; :: thesis: verum

end;

end;

end;