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 & 1 <= i & i <= len I holds

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

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

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

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

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

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

then i in Seg (len I) ;

then A2: i in dom I by FINSEQ_1:def 3;

then I . i in rng I by FUNCT_1:3;

then I /. i in rng I by A2, PARTFUN1:def 6;

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

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

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

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

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

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

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

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

then i in Seg (len I) ;

then A2: i in dom I by FINSEQ_1:def 3;

then I . i in rng I by FUNCT_1:3;

then I /. i in rng I by A2, PARTFUN1:def 6;

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