:: FDIFF_4  semantic presentation begin  




















theorem :: FDIFF_4:1 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:2 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:3 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:4 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:5 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:6 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:7 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:11 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:12 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))  ")" ) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2)))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "c")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:13 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "c")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:14 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  )  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:15 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:16 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  )  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:17 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ))  ")" ) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2)))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x"))))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:18 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:19 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:20 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 3)))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:21 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 3))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:22 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:23 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:26 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" ))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a")) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:27 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:28 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:29 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:30 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:31 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:32 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:33 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:34 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:35 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:36 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "," (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 "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")))) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_taylor_1 :::"#Z"::: )  (Num 2))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_4:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" ) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_4:39 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k6_rfunct_1 :::"^"::: )  )  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:40 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k6_rfunct_1 :::"^"::: )  )  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:41 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:42 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:43 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "x"))))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:44 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:45 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:46 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:47 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_partfun2 :::"id"::: )  (Set (Var "Z")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:48 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:49 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:50 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:51 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:52 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:53 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: FDIFF_4:54 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "n")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "n")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "n")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_prepower :::"#Z"::: )  (Set  "(" (Set (Var "n"))  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_4:55 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Num 1)))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_4:56 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set (Var "f")) ")" ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set (Var "f")) ")" ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set (Var "f")) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_4:57 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" ))) ;