let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL n)
for i being Nat st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
let f be FinSequence of (TOP-REAL n); :: thesis: for i being Nat st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len f implies ( f /. i in rng f & f /. (i + 1) in rng f ) )
assume A1: ( 1 <= i & i + 1 <= len f ) ; :: thesis: ( f /. i in rng f & f /. (i + 1) in rng f )
then A2: i in dom f by SEQ_4:134;
then f . i in rng f by FUNCT_1:3;
hence f /. i in rng f by A2, PARTFUN1:def 6; :: thesis: f /. (i + 1) in rng f
A3: i + 1 in dom f by A1, SEQ_4:134;
then f . (i + 1) in rng f by FUNCT_1:3;
hence f /. (i + 1) in rng f by A3, PARTFUN1:def 6; :: thesis: verum