let i be Element of NAT ; :: according to JORDAN23:def 2 :: thesis: ( 1 <= i & i < len <*x*> implies <*x*> . i <> <*x*> . (i + 1) )
assume ( 1 <= i & i < len <*x*> ) ; :: thesis: <*x*> . i <> <*x*> . (i + 1)
hence <*x*> . i <> <*x*> . (i + 1) by FINSEQ_1:56; :: thesis: verum