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

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

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

then A4:
n <= instr (n,f,g)
by FINSEQ_8:def 10;
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 not g is_substring_of f,n by FINSEQ_8:def 10;

hence contradiction by A3, FINSEQ_8:def 7; :: thesis: verum

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