:: DIFF_2  semantic presentation begin  






















theorem :: DIFF_2:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_diff_1 :::"fdif"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Num 1) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k6_real_1 :::"/"::: )  (Set (Var "h")))))) ; 
 
theorem :: DIFF_2:2 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x")) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" ) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_diff_1 :::"fdif"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Num 2) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))))) ; 
 
theorem :: DIFF_2:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) "," (Set (Var "x")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k7_diff_1 :::"bdif"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Num 1) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k6_real_1 :::"/"::: )  (Set (Var "h")))))) ; 
 
theorem :: DIFF_2:4 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) "," (Set (Var "x")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k7_diff_1 :::"bdif"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Num 2) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))))) ; 
 
theorem :: DIFF_2:5 (Bool  "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:6 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:7 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r1"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ")" ))))) ; 
 
theorem :: DIFF_2:8 (Bool  "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:9 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:10 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r1"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) ) ")" ))))) ; 
 definitionlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); let "x0", "x1", "x2", "x3", "x4" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func :::"[!":::"f" "," "x0" "," "x1" "," "x2" "," "x3" "," "x4":::"!]"::: ->   ($#m1_subset_1 :::"Real":::) equals :: DIFF_2:def 1 (Set (Set  "(" (Set  ($#k11_diff_1 :::"[!"::: ) "f" "," "x0" "," "x1" "," "x2" "," "x3" ($#k11_diff_1 :::"!]"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k11_diff_1 :::"[!"::: ) "f" "," "x1" "," "x2" "," "x3" "," "x4" ($#k11_diff_1 :::"!]"::: ) ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" "x0"  ($#k6_xcmplx_0 :::"-"::: )  "x4" ")" )); end; 










:: deftheorem    defines :::"[!"::: DIFF_2:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k11_diff_1 :::"!]"::: ) ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x4")) ")" ))))); 
 
theorem :: DIFF_2:11 (Bool  "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k1_diff_2 :::"[!"::: ) (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:12 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k1_diff_2 :::"[!"::: ) (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:13 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k1_diff_2 :::"[!"::: ) (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r1"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) ) ")" ))))) ; 
 definitionlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); let "x0", "x1", "x2", "x3", "x4", "x5" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func :::"[!":::"f" "," "x0" "," "x1" "," "x2" "," "x3" "," "x4" "," "x5":::"!]"::: ->   ($#m1_subset_1 :::"Real":::) equals :: DIFF_2:def 2 (Set (Set  "(" (Set  ($#k1_diff_2 :::"[!"::: ) "f" "," "x0" "," "x1" "," "x2" "," "x3" "," "x4" ($#k1_diff_2 :::"!]"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k1_diff_2 :::"[!"::: ) "f" "," "x1" "," "x2" "," "x3" "," "x4" "," "x5" ($#k1_diff_2 :::"!]"::: ) ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" "x0"  ($#k6_xcmplx_0 :::"-"::: )  "x5" ")" )); end; 











:: deftheorem    defines :::"[!"::: DIFF_2:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k2_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k1_diff_2 :::"!]"::: ) ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x5")) ")" ))))); 
 
theorem :: DIFF_2:14 (Bool  "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k2_diff_2 :::"[!"::: ) (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k2_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:15 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k2_diff_2 :::"[!"::: ) (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_diff_2 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k2_diff_2 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) ))))) ; 
 
theorem :: DIFF_2:16 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set  ($#k2_diff_2 :::"[!"::: ) (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r1"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k2_diff_2 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r2"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k2_diff_2 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k2_diff_2 :::"!]"::: ) ) ")" ))))) ; 
 
theorem :: DIFF_2:17 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x0")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x2")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x2")) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x2")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x2"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x2"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: DIFF_2:18 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool  "("  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x0")) ($#k11_diff_1 :::"!]"::: ) )) & (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x3")) "," (Set (Var "x2")) "," (Set (Var "x1")) "," (Set (Var "x0")) ($#k11_diff_1 :::"!]"::: ) ))  ")" ))) ; 
 
theorem :: DIFF_2:19 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool  "("  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x0")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )) & (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x0")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) ))  ")" ))) ; 
 
theorem :: DIFF_2:20 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: DIFF_2:21 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x1")))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: DIFF_2:22 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: DIFF_2:23 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: DIFF_2:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h"))))) ; 
 
theorem :: DIFF_2:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h"))))) ; 
 
theorem :: DIFF_2:26 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h"))))) ; 
 
theorem :: DIFF_2:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" ) & (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x1")))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b")))))) ; 
 
theorem :: DIFF_2:28 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" ) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: DIFF_2:29 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" ) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: DIFF_2:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" ) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4"))  ($#r3_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: DIFF_2:31 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )))))) ; 
 
theorem :: DIFF_2:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )))))) ; 
 
theorem :: DIFF_2:33 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )))))) ; 
 
theorem :: DIFF_2:34 (Bool  "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x1"))) & (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" ) ")" ))))) ; 
 
theorem :: DIFF_2:35 (Bool  "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x2")) ")" ))))) ; 
 
theorem :: DIFF_2:36 (Bool  "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x3")) ")" ) ")" ))))) ; 
 
theorem :: DIFF_2:37 (Bool  "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "x0"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4"))  ($#r3_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set  ($#k1_diff_2 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k1_diff_2 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x3")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x4")) ")" ))))) ; 
 
theorem :: DIFF_2:38 (Bool  "for" (Set (Var "k")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: DIFF_2:39 (Bool  "for" (Set (Var "k")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: DIFF_2:40 (Bool  "for" (Set (Var "k")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k10_real_1 :::"/"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))))) ; 
 
theorem :: DIFF_2:41 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )))) ; 
 
theorem :: DIFF_2:42 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:43 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:44 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:45 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:46 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:47 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:48 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:49 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x0")) ")" ) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )))) ; 
 
theorem :: DIFF_2:50 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:51 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:52 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:53 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" ) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )))) ; 
 
theorem :: DIFF_2:54 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:55 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:56 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:57 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" ) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )))) ; 
 
theorem :: DIFF_2:58 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:59 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:60 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:61 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:62 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 6)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:63 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 6)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:64 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:65 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" )))) ; 
 
theorem :: DIFF_2:66 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_diff_1 :::"fD"::: )   "(" (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 6)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:67 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k4_diff_1 :::"bD"::: )   "(" (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 6)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:68 (Bool  "for" (Set (Var "h")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k5_diff_1 :::"cD"::: )   "(" (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "h"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:69 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k29_sin_cos :::"tan"::: ) )))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  ($#k29_sin_cos :::"tan"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x0")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:70 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k30_sin_cos :::"cot"::: ) )))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  ($#k30_sin_cos :::"cot"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x0")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x1")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:71 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k2_fdiff_9 :::"cosec"::: ) ))) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k2_fdiff_9 :::"cosec"::: ) )))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x0")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" )))) ; 
 
theorem :: DIFF_2:72 (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k1_fdiff_9 :::"sec"::: ) ))) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k1_fdiff_9 :::"sec"::: ) )))) "holds"  (Bool (Set  ($#k9_diff_1 :::"[!"::: ) (Set  ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x0")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) ")" ) ")" )))) ;