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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (p /^ n) or z in rng p )
assume z in rng (p /^ n) ; :: thesis: z in rng p
then consider x being object such that
A1: x in dom (p /^ n) and
A2: z = (p /^ n) . x by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A1;
nx < len (p /^ n) by A1, AFINSQ_1:86;
then A3: nx < (len p) -' n by Def2;

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

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

then (len p) -' n = (len p) - n by XREAL_1:233;
then A4: nx + n in dom p by AFINSQ_1:86, A3, XREAL_1:20;
(p /^ n) . nx = p . (nx + n) by A1, Def2;
hence z in rng p by A2, A4, FUNCT_1:def 3; :: thesis: verum

end;

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

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

end;

end;

end;