let p be FinSequence; :: thesis: for x being object st x in rng p holds
( 1 <= x .. p & x .. p <= len p )
let x be object ; :: 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 Th20;
hence ( 1 <= x .. p & x .. p <= len p ) by FINSEQ_3:25; :: thesis: verum