:: L_HOSPIT  semantic presentation begin  




























theorem :: L_HOSPIT:1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool  "("   "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x0"))) & (Bool (Set (Var "x0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2")))) "holds"  (Bool  "ex" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g1"))) & (Bool (Set (Var "g1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x0"))) & (Bool (Set (Var "g1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "g2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2"))) & (Bool (Set (Var "x0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g2"))) & (Bool (Set (Var "g2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))  ")" ))  ")" )) "holds"  (Bool (Set (Var "f"))  ($#r1_limfunc3 :::"is_convergent_in"::: )  (Set (Var "x0"))))) ; 
 
theorem :: L_HOSPIT:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_limfunc2 :::"is_right_convergent_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_limfunc2 :::"lim_right"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "t"))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "x0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "a")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "x0")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "a"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "t")))  ")" )  ")" )  ")" )  ")" ))) ; 
 
theorem :: L_HOSPIT:3 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_limfunc2 :::"is_left_convergent_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k1_limfunc2 :::"lim_left"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "t"))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x0")))) "holds"  (Bool  "ex" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x0"))) & (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "a")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "x0")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "a"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "t")))  ")" )  ")" )  ")" )  ")" ))) ; 
 
theorem :: L_HOSPIT:4 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st" (Bool (Set (Set (Var "N"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))))) "holds"  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x0"))) & (Bool (Set (Var "x0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2")))) "holds"  (Bool  "ex" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g1"))) & (Bool (Set (Var "g1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x0"))) & (Bool (Set (Var "g1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "g2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2"))) & (Bool (Set (Var "x0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g2"))) & (Bool (Set (Var "g2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))  ")" ))))) ; 
 
theorem :: L_HOSPIT:5 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Set (Var "N"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ))  ($#r2_limfunc3 :::"is_divergent_to+infty_in"::: )  (Set (Var "x0")))  ")" ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r2_limfunc3 :::"is_divergent_to+infty_in"::: )  (Set (Var "x0"))))) ; 
 
theorem :: L_HOSPIT:6 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Set (Var "N"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ))  ($#r3_limfunc3 :::"is_divergent_to-infty_in"::: )  (Set (Var "x0")))  ")" ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r3_limfunc3 :::"is_divergent_to-infty_in"::: )  (Set (Var "x0"))))) ; 
 
theorem :: L_HOSPIT:7 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")) ")" ))) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "f"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "g"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ))  ($#r4_limfunc2 :::"is_right_convergent_in"::: )  (Set (Var "x0")))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r4_limfunc2 :::"is_right_convergent_in"::: )  (Set (Var "x0"))) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k2_limfunc2 :::"lim_right"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_limfunc2 :::"lim_right"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x0")) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) "," (Set (Var "x0")) ")" ))  ")" ))  ")" ))) ; 
 
theorem :: L_HOSPIT:8 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")) ")" ))) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "f"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "g"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) ) ")" ))  ($#r1_limfunc2 :::"is_left_convergent_in"::: )  (Set (Var "x0")))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r1_limfunc2 :::"is_left_convergent_in"::: )  (Set (Var "x0"))) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_limfunc2 :::"lim_left"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_limfunc2 :::"lim_left"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "x0")) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) "," (Set (Var "x0")) ")" ))  ")" ))  ")" ))) ; 
 
theorem :: L_HOSPIT:9 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Set (Var "N"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ))  ($#r1_limfunc3 :::"is_convergent_in"::: )  (Set (Var "x0")))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r1_limfunc3 :::"is_convergent_in"::: )  (Set (Var "x0"))) & (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st" (Bool (Set   ($#k1_limfunc3 :::"lim"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_limfunc3 :::"lim"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ) ")" ) "," (Set (Var "x0")) ")" )))  ")" ))) ; 
 
theorem :: L_HOSPIT:10 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "N"))) & (Bool (Set (Set (Var "N"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "N")) ")" ))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0")))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r1_limfunc3 :::"is_convergent_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k1_limfunc3 :::"lim"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")"  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "g")) "," (Set (Var "x0")) ")"  ")" )))  ")" ))) ;