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:11;
then (instr n,f,g) -' 1 >= len f by XREAL_0:def 2;
then f /^ ((instr n,f,g) -' 1) = {} by FINSEQ_5:35;
then A3: len (f /^ ((instr n,f,g) -' 1)) < 1 ;
instr n,f,g > 0 by A2, NAT_1:2;
then ( len g >= 0 & f /^ ((instr n,f,g) -' 1) is_preposition_of ) by FINSEQ_8:def 10, NAT_1:2;
then g = {} by A3, FINSEQ_8:def 8;
hence contradiction by A1, A2, Th38; :: thesis: verum