let n be Element of NAT ; :: thesis: for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
let p be FinSequence; :: thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) )
assume A1: n < len p ; :: thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
n >= 0 by NAT_1:2;
then A3: n + 1 >= 0 + 1 by XREAL_1:9;
n + 1 <= len p by A1, NAT_1:13;
then n + 1 in dom p by A3, FINSEQ_3:27;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def 5; :: thesis: verum