:: ROLLE  semantic presentation begin  




























theorem :: ROLLE:1 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool  "ex" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: ROLLE:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "t")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: ROLLE:3 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool  "ex" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k9_real_1 :::"-"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ROLLE:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "t")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" ) ")" ) ")"  ")" ) ")" )))  ")" )))) ; 
 
theorem :: ROLLE:5 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))) "holds"  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "f1"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "f2"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool  "ex" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x0")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" )))  ")" )))) ; 
 
theorem :: ROLLE:6 (Bool  "for" (Set (Var "x")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "t")))) "holds"  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "f1"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "f2"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x1")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "t")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" ) ")" ) ")"  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" ) ")" ) ")"  ")" )))  ")" )))) ; 
 
theorem :: ROLLE:7 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is" bbbadV3_FUNCT_1()))) ; 
 
theorem :: ROLLE:8 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f1"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "f2"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is" bbbadV3_FUNCT_1()) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r"))))))  ")" ))) ; 
 
theorem :: ROLLE:9 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v5_valued_0 :::"increasing"::: )  ))) ; 
 
theorem :: ROLLE:10 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v6_valued_0 :::"decreasing"::: )  ))) ; 
 
theorem :: ROLLE:11 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v7_valued_0 :::"non-decreasing"::: )  ))) ; 
 
theorem :: ROLLE:12 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ))) ;