("derivatives_con" |derivatives_con| |IMP_derivatives_ax_TCC1| "" (SKOSIMP*) (("" (LEMMA "connected_domain") (("" (INST?) (("" (INST -1 "y!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)("derivatives_con" |derivatives_con| |IMP_derivatives_ax_TCC2| "" (SKOSIMP*) (("" (LEMMA "not_one_element") (("" (INST?) NIL NIL)) NIL)) NIL)("derivatives_ax" |derivatives_ax| |caret_TCC1| "" (SUBTYPE-TCC) NIL NIL)("chain_rule_ax" |chain_rule_ax| |deriv_comp_fun_TCC5| "" (ASSUMING-TCC))("chain_rule_ax" |chain_rule_ax| |deriv_comp_fun_TCC4| "" (ASSUMING-TCC))("chain_rule_ax" |chain_rule_ax| |deriv_comp_fun_TCC3| "" (ASSUMING-TCC))("chain_rule_ax" |chain_rule_ax| |deriv_comp_fun_TCC2| "" (ASSUMING-TCC))("chain_rule_ax" |chain_rule_ax| |deriv_comp_fun_TCC1| "" (SUBTYPE-TCC))("chain_rule_ax" |chain_rule_ax| |gg_TCC2| "" (ASSUMING-TCC))("chain_rule_ax" |chain_rule_ax| |gg_TCC1| "" (ASSUMING-TCC))("derivatives_con" |derivatives_con| |IMP_derivatives_TCC1| "" (ASSUMING-TCC))("derivatives_con" |derivatives_con| |IMP_derivatives_TCC2| "" (ASSUMING-TCC))