theorem Th2: :: RADIX_5:2

for i, n being Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n