let m be non zero Element of NAT ; :: thesis: for I being non empty FinSequence of NAT

for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds

( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

let I be non empty FinSequence of NAT ; :: thesis: for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds

( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

let i be Element of NAT ; :: thesis: ( rng I c= Seg m & i <= (len I) - 1 implies ( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) )

assume A1: rng I c= Seg m ; :: thesis: ( not i <= (len I) - 1 or ( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) )

assume A2: i <= (len I) - 1 ; :: thesis: ( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

A3: 0 + 1 <= i + 1 by XREAL_1:6;

i + 1 <= ((len I) - 1) + 1 by A2, XREAL_1:6;

then i + 1 in Seg (len I) by A3;

then A4: i + 1 in dom I by FINSEQ_1:def 3;

then I . (i + 1) in rng I by FUNCT_1:3;

then I /. (i + 1) in rng I by A4, PARTFUN1:def 6;

hence ( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) by FINSEQ_1:1, A1; :: thesis: verum

for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds

( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

let I be non empty FinSequence of NAT ; :: thesis: for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds

( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

let i be Element of NAT ; :: thesis: ( rng I c= Seg m & i <= (len I) - 1 implies ( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) )

assume A1: rng I c= Seg m ; :: thesis: ( not i <= (len I) - 1 or ( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) )

assume A2: i <= (len I) - 1 ; :: thesis: ( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

A3: 0 + 1 <= i + 1 by XREAL_1:6;

i + 1 <= ((len I) - 1) + 1 by A2, XREAL_1:6;

then i + 1 in Seg (len I) by A3;

then A4: i + 1 in dom I by FINSEQ_1:def 3;

then I . (i + 1) in rng I by FUNCT_1:3;

then I /. (i + 1) in rng I by A4, PARTFUN1:def 6;

hence ( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) by FINSEQ_1:1, A1; :: thesis: verum