continuous_functions_more [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%
%  Additions made by Ricky W. Butler    NASA Langley
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING

     connected_domain : ASSUMPTION
 FORALL (x, y : T), (z : real) :
     x <= z AND z <= y IMPLIES T_pred(z)

     not_one_element : ASSUMPTION
  FORALL (x : T) : EXISTS (y : T) : x /= y

   ENDASSUMING


  IMPORTING continuous_functions[T], convergence_sequences


  f: VAR [T -> real]
  a,b,c: VAR T
  cn: VAR sequence[T]
  n: VAR nat


  convergence_fun_of  : LEMMA convergence(cn,c) AND
                               continuous?(f,c) IMPLIES  % move to analysis
                                 convergence(LAMBDA n: f(cn(n)),f(c))
  

  IMPORTING unif_cont_fun   %% to maintain upward compatibility

END continuous_functions_more