begin
theorem
canceled;
theorem Th2:
:: deftheorem Def1 defines uniformly_continuous UNIFORM1:def 1 :
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
begin
theorem Th8:
Lm1:
Closed-Interval-TSpace 0 ,1 = TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:def 8;
Lm2:
I[01] = TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:27, TOPMETR:def 8;
Lm3:
the carrier of I[01] = the carrier of (Closed-Interval-MSpace 0 ,1)
by Lm1, TOPMETR:16, TOPMETR:27;
theorem
theorem
begin
theorem
Lm4:
for x being set
for f being FinSequence holds
( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
Lm5:
for x being set
for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
theorem
canceled;
theorem Th13:
Lm6:
for r, s1, s2 being Real holds
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
theorem Th14:
:: deftheorem Def2 defines decreasing UNIFORM1:def 2 :
Lm7:
for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) holds
f is increasing
Lm8:
for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) holds
f is decreasing
theorem
theorem