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

suppose n > len f ; :: thesis: f /^ n is integer-yielding

hence f /^ n is integer-yielding by RFINSEQ:def 2; :: thesis: verum

end;

suppose Q1: n <= len f ; :: thesis: f /^ n is integer-yielding

then Q: ( len (f /^ n) = (len f) - n & ( for m being Nat st m in dom (f /^ n) holds
(f /^ n) . m = f . (m + n) ) ) by RFINSEQ:def 2;

now

let u be set ; :: thesis: ( u in rng (f /^ n) implies u in INT )
assume AS: u in rng (f /^ n) ; :: thesis: u in INT
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
consider x being set such that
H: ( x in dom (f /^ n) & (f /^ n) . x = u ) by AS, FUNCT_1:def 5;
reconsider k = (len f) - n as Element of NAT by Q1, INT_1:18;
reconsider k = k as natural number ;
dom (f /^ n) = Seg k by Q, FINSEQ_1:def 3;
then consider x' being Element of NAT such that
X: ( x' = x & 1 <= x' & x' <= k ) by H;
reconsider x = x as Element of NAT by X;
reconsider f' = f as FinSequence of INT by intint;
I: x + n' in dom f' by H, FINSEQ_5:29;
K: (f /^ n) . x = f . (x + n) by H, Q1, RFINSEQ:def 2;
L: f . (x + n) in rng f by I, FUNCT_1:def 5;
rng f c= INT by VALUED_0:def 5;
hence u in INT by H, K, L; :: thesis: verum

end;

then rng (f /^ n) c= INT by TARSKI:def 3;
hence f /^ n is integer-yielding by VALUED_0:def 5; :: thesis: verum

end;

end;