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
A2: len g >= 0 by NAT_1:2;
assume A3: instr n,f,g > len f ; :: thesis: contradiction
then A4: instr n,f,g >= (len f) + 1 by NAT_1:13;
instr n,f,g > 0 by A3, NAT_1:2;
then A5: ( n <= instr n,f,g & f /^ ((instr n,f,g) -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= instr n,f,g ) ) by FINSEQ_8:def 10;
A6: (instr n,f,g) - 1 >= ((len f) + 1) - 1 by A4, XREAL_1:11;
(instr n,f,g) -' 1 >= len f by A6, XREAL_0:def 2;
then f /^ ((instr n,f,g) -' 1) = {} by FINSEQ_5:35;
then len (f /^ ((instr n,f,g) -' 1)) < 1 ;
then len g = 0 by A2, A5, FINSEQ_8:def 8;
then g = {} ;
hence contradiction by A1, A3, Th38; :: thesis: verum