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