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

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