vect_chain_rule [ T1, T2 : TYPE FROM real ] : THEORY
BEGIN

  ASSUMING
    IMPORTING analysis@deriv_domain_def

    deriv_domain1    : ASSUMPTION deriv_domain?[T1]

    not_one_element1 : ASSUMPTION not_one_element?[T1]

    deriv_domain2    : ASSUMPTION deriv_domain?[T2]

    not_one_element2 : ASSUMPTION not_one_element?[T2]

  ENDASSUMING

  IMPORTING analysis@derivative_props, analysis@lim_of_composition, 
            vect_deriv_2D, analysis@chain_rule

  f: VAR [T1 -> T2]
  g : VAR [T2 -> Vect2]
  x : VAR T1
  DF, DG : VAR real

  composition_derivable_vfun : LEMMA derivable?(f) AND differentiable_rv?(g) 
                                       IMPLIES differentiable_rv?(g o f)

  ff : VAR { f | derivable?(f) }
  gg : VAR { g | differentiable_rv?(g) }

  IMPORTING vect_fun_ops_rv

  h: VAR [T1 -> Vect2]

  deriv_comp_vfun : LEMMA deriv(gg o ff) = deriv(ff)*(deriv(gg) o ff) 

END vect_chain_rule