:: FDIFF_6  semantic presentation begin  


















theorem :: FDIFF_6:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x"))))) ; 
 
theorem :: FDIFF_6:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: FDIFF_6: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 "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"))  ($#k47_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"))  ($#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  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6: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 "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  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (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_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (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  "(" (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (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  "(" (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6: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")) "," (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 (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (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"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (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 (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_newton :::"|^"::: )  (Num 4) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 4) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6: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")) "," (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  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k3_rfunct_1 :::"/"::: )  (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"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#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  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#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  "(" (Set (Var "a"))  ($#k2_newton :::"|^"::: )  (Num 4) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Num 4) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:7 (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_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f2"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f1")) ")" ) ")" ))) & (Bool (Set (Var "f1"))  ($#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 "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f2"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f1")) ")" ))  ($#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_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f2"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f1")) ")" ) ")" )  ($#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  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:8 (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 :::"/"::: )  (Num 2) ")" )  ($#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  "(" (Set (Var "f2"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f1")) ")" ) ")" ))) & (Bool (Set (Var "f1"))  ($#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 "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#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 :::"/"::: )  (Num 2) ")" )  ($#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 (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:9 (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  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" ) ")" ))) & (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 (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" ))  ($#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  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:10 (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f2")) "," (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 (Var "f2"))  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k3_valued_1 :::"+"::: )  (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 "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f2"))  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k3_valued_1 :::"+"::: )  (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  "(" (Set (Var "f2"))  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k3_valued_1 :::"+"::: )  (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 (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:11 (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  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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 (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:12 (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" )  ($#k20_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  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )))  ")" )  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" )  ($#k20_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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:13 (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 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k20_valued_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 (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  ($#k8_power :::"number_e"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k20_valued_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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:14 (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"::: ) )  ($#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   ($#k1_real_1 :::"-"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:15 (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"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (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  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set (Var "x"))))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (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"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6: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  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )))  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6: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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" ) ")" )  ($#k20_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  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ))) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )))  ")" )  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" ) ")" )  ($#k20_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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" )  ($#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"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6: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 "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 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (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 (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k8_power :::"number_e"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (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 (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6: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 "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 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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 (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k8_power :::"number_e"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:20 (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_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_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_valued_1 :::"+"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:21 (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"::: ) )  ($#k47_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  "("  (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  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_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"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:22 (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  "(" (Set (Var "f"))  ($#k47_valued_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 (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#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 "f"))  ($#k47_valued_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  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:23 (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  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (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  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (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  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (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 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:24 (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#k3_valued_1 :::"+"::: )  (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 (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_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  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_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 (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:25 (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  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#k47_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  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#k47_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  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:26 (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#k47_valued_1 :::"-"::: )  (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 :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_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  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_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 (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:27 (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_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_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  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_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_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:28 (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 (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f1")) ")" ) ")" )  ($#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 "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set (Var "f1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (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 (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:29 (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_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (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  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (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  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (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 (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:30 (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 (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set (Var "f1")) ")" ) ")" )  ($#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 (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "("  (Bool (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 (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (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_6:31 (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_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k47_valued_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 (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k47_valued_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  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:32 (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 (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k47_valued_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 "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (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 (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:33 (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 (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_rfunct_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 2) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f1"))  ($#k3_valued_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 (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "("  (Bool (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 (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:34 (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  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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 (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set (Var "x"))))  ")" )) "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 (Set  "(" (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:35 (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  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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   ($#k1_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 (Set  "(" (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k26_sin_cos :::"exp_R"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6: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")) "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  "(" (Set (Var "f"))  ($#k3_valued_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 (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "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  "(" (Set (Var "f"))  ($#k3_valued_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  "(" (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  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:37 (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  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#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 "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" )))  ")" )  ")" ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 2)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" ) ")" ) ")" ))  ($#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  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "a")) ")"  ")" ) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1")) ")" ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k10_prepower :::"#R"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:38 (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 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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 (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:39 (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  "(" (Set (Var "f"))  ($#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 (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (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)) & (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 (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#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  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_taylor_1 :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:40 (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  "(" (Set (Var "f"))  ($#k3_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 (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (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)) & (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  "("  ($#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  "(" (Set (Var "f"))  ($#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  "("  ($#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  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_prepower :::"#R"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:41 (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k26_valued_1 :::"(#)"::: )  (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 (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_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  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k26_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 (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:42 (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_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k3_taylor_1 :::"ln"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k26_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 (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) & (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 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k26_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  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k26_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 (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6:43 (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 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:44 (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 "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 (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x"))))  ")" )  ")" ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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 (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:45 (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 "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 (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "("  (Bool (Set (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x"))))  ")" )  ")" ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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 (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k26_valued_1 :::"(#)"::: )  (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  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ))  ")" )  ")" )))) ; 
 
theorem :: FDIFF_6:46 (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  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" ))) & (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  ($#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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "n")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Set (Var "n")) ")" )  ($#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  "(" (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_prepower :::"#Z"::: )  (Set  "(" (Set (Var "n"))  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FDIFF_6: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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 3) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 3) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" )  ($#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 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 3) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" )  ($#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  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k2_newton :::"|^"::: )  (Num 3)))  ")" )  ")" )) ; 
 
theorem :: FDIFF_6: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  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 3) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 3) ")" )  ($#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 3) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k1_taylor_1 :::"#Z"::: )  (Num 3) ")" )  ($#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")) ")" )  ($#k2_newton :::"|^"::: )  (Num 3)))  ")" )  ")" )) ; 
 
theorem :: FDIFF_6: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  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k3_taylor_1 :::"ln"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k3_taylor_1 :::"ln"::: ) ))  ($#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  ($#k3_taylor_1 :::"ln"::: ) ) ")" )  ($#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  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")"  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" )  ")" )) ; 
 
theorem :: FDIFF_6: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  "("  ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k3_taylor_1 :::"ln"::: ) ) ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k3_taylor_1 :::"ln"::: ) ) ")" ))  ($#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  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k3_taylor_1 :::"ln"::: ) ) ")" ) ")" )  ($#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  "("  ($#k6_power :::"log"::: )   "(" (Set  ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")"  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" )  ")" )) ;