let n be 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 ) )
A1: n + 1 >= 0 + 1 by XREAL_1:7;
assume n < len p ; :: thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
then n + 1 <= len p by NAT_1:13;
then n + 1 in dom p by A1, FINSEQ_3:25;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def 3; :: thesis: verum