let n be Element of NAT ; :: thesis: for f being FinSequence of (TOP-REAL n)
for i being Element of 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 Element of NAT st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
let i be Element of 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 + 1 in dom f by GOBOARD2:3;
A3: i in dom f by A1, GOBOARD2:3;
then f . i in rng f by FUNCT_1:12;
hence f /. i in rng f by A3, PARTFUN1:def 8; :: thesis: f /. (i + 1) in rng f
f . (i + 1) in rng f by A2, FUNCT_1:12;
hence f /. (i + 1) in rng f by A2, PARTFUN1:def 8; :: thesis: verum