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