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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng (p /^ n) ; :: thesis:
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;

suppose n < len p ; :: thesis:

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:

end;

suppose n >= len p ; :: thesis:

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

end;

end;

end;