theorem Th18: :: KURATO_0:18

for f being Function st ( for i being Nat holds f . (i + 1) c= f . i ) holds
for i, j being Nat st i <= j holds
f . j c= f . i