let D be non empty set ; for f, g being File of D
for n being Element of NAT st 0 < n & n <= len f holds
instr (n,f,g) <= len f
let f, g be File of D; for n being Element of NAT st 0 < n & n <= len f holds
instr (n,f,g) <= len f
let n be Element of NAT ; ( 0 < n & n <= len f implies instr (n,f,g) <= len f )
assume A1:
( 0 < n & n <= len f )
; instr (n,f,g) <= len f
assume A2:
instr (n,f,g) > len f
; contradiction
then
instr (n,f,g) >= (len f) + 1
by NAT_1:13;
then
(instr (n,f,g)) - 1 >= ((len f) + 1) - 1
by XREAL_1:9;
then
(instr (n,f,g)) -' 1 >= len f
by XREAL_0:def 2;
then
f /^ ((instr (n,f,g)) -' 1) = {}
by FINSEQ_5:32;
then A3:
len (f /^ ((instr (n,f,g)) -' 1)) < 1
;
instr (n,f,g) > 0
by A2;
then
( len g >= 0 & g is_preposition_of f /^ ((instr (n,f,g)) -' 1) )
by FINSEQ_8:def 10;
then
g = {}
by A3, FINSEQ_8:def 8;
hence
contradiction
by A1, A2, Th37; verum