let D be non empty set ; 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; for n being Element of NAT st 0 < n & g = {} holds
instr (n,f,g) = n
let n be Element of NAT ; ( 0 < n & g = {} implies instr (n,f,g) = n )
assume that
A1:
0 < n
and
A2:
g = {}
; instr (n,f,g) = n
A3:
len g = 0
by A2;
instr (n,f,g) <> 0
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; verum