restriction_derivatives2[T1, T2 : TYPE FROM real] : THEORY BEGIN ASSUMING connected_domain_T1 : ASSUMPTION FORALL (x, y : T1), (z : real) : x <= z AND z <= y IMPLIES T1_pred(z) connected_domain_T2 : ASSUMPTION FORALL (x, y : T2), (z : real) : x <= z AND z <= y IMPLIES T2_pred(z) not_one_element_T1 : ASSUMPTION FORALL (x : T1) : EXISTS (y : T1) : x /= y not_one_element_T2 : ASSUMPTION FORALL (x : T2) : EXISTS (y : T2) : x /= y sub_domain : ASSUMPTION FORALL (x : T1) : EXISTS (y : T2) : x = y ENDASSUMING IMPORTING derivatives f : VAR deriv_fun[T2] a : VAR T1 sub_dom : JUDGEMENT T1 SUBTYPE_OF T2 % LEMMA FORALL (u : T1) : T2_pred(u) restrict2(f) : [T1 -> real] = LAMBDA (u : T1) : f(u) CONVERSION restrict2 restrict_differentiable2 : AXIOM derivable[T1](f) restrict_derivative2 : AXIOM deriv(f)(a) = deriv[T1](f)(a) END restriction_derivatives2