let a, b be Real; :: thesis: for s being Real_Sequence st rng s c= [.a,b.] holds

s is sequence of (Closed-Interval-MSpace (a,b))

let s be Real_Sequence; :: thesis: ( rng s c= [.a,b.] implies s is sequence of (Closed-Interval-MSpace (a,b)) )

assume A1: rng s c= [.a,b.] ; :: thesis: s is sequence of (Closed-Interval-MSpace (a,b))

reconsider t = s . 0 as Real ;

A2: dom s = NAT by FUNCT_2:def 1;

then s . 0 in rng s by FUNCT_1:def 3;

then ( a <= t & t <= b ) by A1, XXREAL_1:1;

then the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by TOPMETR:10, XXREAL_0:2;

hence s is sequence of (Closed-Interval-MSpace (a,b)) by A1, A2, FUNCT_2:2; :: thesis: verum

s is sequence of (Closed-Interval-MSpace (a,b))

let s be Real_Sequence; :: thesis: ( rng s c= [.a,b.] implies s is sequence of (Closed-Interval-MSpace (a,b)) )

assume A1: rng s c= [.a,b.] ; :: thesis: s is sequence of (Closed-Interval-MSpace (a,b))

reconsider t = s . 0 as Real ;

A2: dom s = NAT by FUNCT_2:def 1;

then s . 0 in rng s by FUNCT_1:def 3;

then ( a <= t & t <= b ) by A1, XXREAL_1:1;

then the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by TOPMETR:10, XXREAL_0:2;

hence s is sequence of (Closed-Interval-MSpace (a,b)) by A1, A2, FUNCT_2:2; :: thesis: verum