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;
g is_preposition_of f /^ (n -' 1) 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