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 that
A1: 0 < n and
A2: g = {} ; :: thesis: instr n,f,g = n
A3: len g = 0 by A2;
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 A3, FINSEQ_8:def 7; :: thesis: verum

end;

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