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
A1: x in dom (f /^ n) and
A2: z = (f /^ n) . x by FUNCT_1:def 5;
reconsider nx = x as Element of NAT by A1;
nx < len (f /^ n) by A1, NAT_1:45;
then A3: nx < (len f) -' n by Def2;

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

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

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

end;

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

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

end;

end;

end;