theorem Th5: :: INTEGRA1:7

for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D & i <> 1 holds
( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )