let D be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 0 < n & n <= len f implies instr (n,f,g) <= len f )
assume A1: ( 0 < n & n <= len f ) ; :: thesis: instr (n,f,g) <= len f
assume A2: instr (n,f,g) > len f ; :: thesis: 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; :: thesis: verum