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

end;

suppose A1:
n <= len f
; :: thesis: f /^ n is INT -valued

hence f /^ n is INT -valued by RELAT_1:def 19; :: thesis: verum

end;

now :: thesis: for u being object st u in rng (f /^ n) holds

u in INT

then
rng (f /^ n) c= INT
by TARSKI:def 3;u in INT

reconsider f9 = f as FinSequence of INT by Lm1;

let u be object ; :: 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 RELAT_1:def 19;

assume u in rng (f /^ n) ; :: thesis: u in INT

then consider x being object 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;let u be object ; :: 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 RELAT_1:def 19;

assume u in rng (f /^ n) ; :: thesis: u in INT

then consider x being object 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

hence f /^ n is INT -valued by RELAT_1:def 19; :: thesis: verum