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 1; :: thesis: verum

end;

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

now

reconsider f9 = f as FinSequence of INT by Lm1;
let u be set ; :: thesis: ( u in rng (f /^ n) implies u in INT )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
A2: rng f c= INT by VALUED_0:def 5;
assume u in rng (f /^ n) ; :: thesis: u in INT
then consider x being set such that
A3: x in dom (f /^ n) and
A4: (f /^ n) . x = u by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A3;
x + n9 in dom f9 by A3, FINSEQ_5:26;
then A5: f . (x + n) in rng f by FUNCT_1:def 3;
(f /^ n) . x = f . (x + n) by A1, A3, RFINSEQ:def 1;
hence u in INT by A4, A5, A2; :: 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;