let D be non empty set ; :: thesis: for f, g being File of D
for n being Element of NAT st 0 < n & g = {} holds
instr n,f,g = n
let f, g be File of D; :: thesis: for n being Element of NAT st 0 < n & g = {} holds
instr n,f,g = n
let n be Element of NAT ; :: thesis: ( 0 < n & g = {} implies instr n,f,g = n )
assume A1: ( 0 < n & g = {} ) ; :: thesis: instr n,f,g = n
then A2: len g = 0 ;
instr n,f,g <> 0

proof

assume instr n,f,g = 0 ; :: thesis: contradiction
then not g is_substring_of f,n by FINSEQ_8:def 10;
hence contradiction by A2, FINSEQ_8:def 7; :: thesis: verum

end;

then A3: ( 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;
f /^ (n -' 1) is_preposition_of by A2, FINSEQ_8:def 8;
then n >= instr n,f,g by A1, FINSEQ_8:def 10;
hence instr n,f,g = n by A3, XXREAL_0:1; :: thesis: verum