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