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