let a, b be real number ; :: 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)
A2: dom s = NAT by FUNCT_2:def 1;
then A3: s . 0 in rng s by FUNCT_1:def 5;
reconsider t = s . 0 as Real ;
( a <= t & t <= b ) by A1, A3, XXREAL_1:1;
then the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] by TOPMETR:14, XXREAL_0:2;
hence s is sequence of (Closed-Interval-MSpace a,b) by A1, A2, FUNCT_2:4; :: thesis: verum