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

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