let p be FinSequence; :: thesis: for x being set st x in rng p holds
( 1 <= x .. p & x .. p <= len p )
let x be set ; :: thesis: ( x in rng p implies ( 1 <= x .. p & x .. p <= len p ) )
assume x in rng p ; :: thesis: ( 1 <= x .. p & x .. p <= len p )
then x .. p in dom p by Th30;
hence ( 1 <= x .. p & x .. p <= len p ) by FINSEQ_3:27; :: thesis: verum