theorem Th37: :: FILEREC1:37

for D being 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