integral_diff_doms[T: TYPE+ FROM real, U: TYPE+ FROM real]: THEORY
%----------------------------------------------------------------------------
%
%  Integral of two functions that are identical over the integration
%  range and have different domains are shown to be equal.
%
%  Author:  Rick Butler     NASA Langley Research Center
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING deriv_domain_def

      connected_domain : ASSUMPTION connected?[T]

      not_one_element  : ASSUMPTION not_one_element?[T]

      con_dom_U        : ASSUMPTION  connected?[U]

      not_one_U        : ASSUMPTION not_one_element?[U]

   ENDASSUMING

   IMPORTING integral


   f: VAR [T -> real]
   g: VAR [U -> real]

   a,b: VAR real

   int_diff_dom: LEMMA T_pred(a) AND T_pred(b) AND
                       U_pred(a) AND U_pred(b) AND a < b AND
                       integrable?[T](a,b,f) AND integrable?[U](a, b, g) AND
                   (FORALL (x: real): x >= a AND x <= b IMPLIES f(x) = g(x)) 
               IMPLIES
                    integral(a,b,f) = integral(a,b,g)


   Int_diff_dom: LEMMA T_pred(a) AND T_pred(b) AND
                       U_pred(a) AND U_pred(b) AND
                       Integrable?[T](a,b,f) AND Integrable?[U](a, b, g) AND
                   (FORALL (x: Closed_interval[real](a,b)): f(x) = g(x)) 
               IMPLIES
                    Integral(a,b,f) = Integral(a,b,g)
                   

END integral_diff_doms