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

( (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