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