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

( 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