for a, b being Real
for s being Real_Sequence st rng s c= [.a,b.] holds
s is sequence of (Closed-Interval-MSpace (a,b))