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 )
A2: n >= 0 by NAT_1:2;
A3: n + 1 >= 0 + 1 by A2, XREAL_1:9;
A4: n + 1 <= len p by A1, NAT_1:13;
A5: n + 1 in dom p by A3, A4, FINSEQ_3:27;
thus ( n + 1 in dom p & p . (n + 1) in rng p ) by A5, FUNCT_1:def 5; :: thesis: verum