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 GOBOARD2:def 2;
then consider x being set such that
A1: ( x in dom (Incr g) & (Incr g) . x = r ) by FUNCT_1:def 5;
A2: x in Seg (len (Incr g)) by A1, FINSEQ_1:def 3;
reconsider j = x as Element of NAT by A1;
A3: ( 1 <= j & j <= len (Incr g) ) by A2, FINSEQ_1:3;
then A4: 1 <= len (Incr g) by XXREAL_0:2;
then 1 in dom (Incr g) by FINSEQ_3:27;
hence (Incr g) . 1 <= r by A1, A3, GOBOARD2:18; :: thesis: r <= (Incr g) . (len (Incr g))
len (Incr g) in dom (Incr g) by A4, FINSEQ_3:27;
hence r <= (Incr g) . (len (Incr g)) by A1, A3, GOBOARD2:18; :: thesis: verum