chain_rule_ax [ T1, T2 : TYPE FROM real ] : THEORY BEGIN ASSUMING connected_domain1 : ASSUMPTION FORALL (x, y : T1), (z : real) : x <= z AND z <= y IMPLIES T1_pred(z) not_one_element1 : ASSUMPTION FORALL (x : T1) : EXISTS (y : T1) : x /= y connected_domain2 : ASSUMPTION FORALL (x, y : T2), (z : real) : x <= z AND z <= y IMPLIES T2_pred(z) not_one_element2 : ASSUMPTION FORALL (x : T2) : EXISTS (y : T2) : x /= y ENDASSUMING IMPORTING derivatives_ax f : VAR [T1 -> T2] g : VAR [T2 -> real] x : VAR T1 composition_derivable : AXIOM derivable(f, x) AND derivable(g, f(x)) IMPLIES derivable(g o f, x) deriv_composition : AXIOM derivable(f, x) AND derivable(g, f(x)) IMPLIES deriv(g o f, x) = deriv(g, f(x)) * deriv(f, x) % ff : VAR { f | derivable(f) } % gg : VAR { g | derivable(g) } % deriv_comp_fun : LEMMA % deriv(gg o ff) = (deriv(gg) o ff) * deriv(ff) END chain_rule_ax