theorem :: FILEREC1:38

for D being non empty set
for f, g being File of D
for n being Element of NAT st 0 < n & n <= len f holds
instr (n,f,g) <= len f