let p be FinSequence; :: thesis: for x being object st x in rng p holds
( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT )
let x be object ; :: thesis: ( x in rng p implies ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) )
assume x in rng p ; :: thesis: ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT )
then ( 1 <= x .. p & x .. p <= len p ) by Th21;
hence ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) by INT_1:5; :: thesis: verum