let r be Real; :: thesis: for g being FinSequence of REAL st r in rng g holds
( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )
let g be FinSequence of REAL ; :: thesis: ( r in rng g implies ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) ) )
assume r in rng g ; :: thesis: ( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )
then r in rng (Incr g) by SEQ_4:def 21;
then consider x being object such that
A1: x in dom (Incr g) and
A2: (Incr g) . x = r by FUNCT_1:def 3;
reconsider j = x as Nat by A1;
A3: x in Seg (len (Incr g)) by A1, FINSEQ_1:def 3;
then A4: j <= len (Incr g) by FINSEQ_1:1;
A5: 1 <= j by A3, FINSEQ_1:1;
then A6: 1 <= len (Incr g) by A4, XXREAL_0:2;
then 1 in dom (Incr g) by FINSEQ_3:25;
hence (Incr g) . 1 <= r by A1, A2, A5, SEQ_4:137; :: thesis: r <= (Incr g) . (len (Incr g))
len (Incr g) in dom (Incr g) by A6, FINSEQ_3:25;
hence r <= (Incr g) . (len (Incr g)) by A1, A2, A4, SEQ_4:137; :: thesis: verum