:: INTEGRA8  semantic presentation begin  





















theorem :: INTEGRA8:1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")))))) ; 
 
theorem :: INTEGRA8:2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: INTEGRA8:3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")))))) ; 
 
theorem :: INTEGRA8:4 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: INTEGRA8:5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))) ; 
 
theorem :: INTEGRA8:6 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:7 (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 4) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2))) ; 
 
theorem :: INTEGRA8:8 (Bool (Set   ($#k18_sin_cos :::"sin"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 4) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))) ; 
 
theorem :: INTEGRA8:9 (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) ; 
 
theorem :: INTEGRA8:10 (Bool (Set   ($#k3_sin_cos6 :::"arcsin"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 4))) ; 
 
theorem :: INTEGRA8:11 (Bool (Set   ($#k3_sin_cos6 :::"arcsin"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 4) ")" ))) ; 
 
theorem :: INTEGRA8:12 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "x"))  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )))) ; 
 
theorem :: INTEGRA8:13 (Bool (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 4) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2))) ; 
 
theorem :: INTEGRA8:14 (Bool (Set   ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 4) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))) ; 
 
theorem :: INTEGRA8:15 (Bool (Set   ($#k6_sin_cos6 :::"arccos"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 4))) ; 
 
theorem :: INTEGRA8:16 (Bool (Set   ($#k6_sin_cos6 :::"arccos"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 4))) ; 
 
theorem :: INTEGRA8:17 (Bool (Set (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k8_power :::"number_e"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" ))) ; 
 
theorem :: INTEGRA8:18 (Bool (Set (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: INTEGRA8:19 (Bool (Set (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k8_power :::"number_e"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" ))) ; 
 
theorem :: INTEGRA8:20 (Bool  "for" (Set (Var "L1")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "holds"  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "L1"))) "is"   ($#m1_subset_1 :::"LinearFunc":::))) ; 
 
theorem :: INTEGRA8:21 (Bool  "for" (Set (Var "R1")) "being"   ($#m1_subset_1 :::"RestFunc":::) "holds"  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "R1"))) "is"   ($#m1_subset_1 :::"RestFunc":::))) ; 
 
theorem :: INTEGRA8:22 (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_fdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "f1")))  ($#r1_fdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "f1")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" )))  ")" ))) ; 
 
theorem :: INTEGRA8:23 (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (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 (Var "f1")) ")" ))) & (Bool (Set (Var "f1"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set   ($#k32_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  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "f1")) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k1_fdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" ))) ; 
 
theorem :: INTEGRA8:24 (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) ; 
 
theorem :: INTEGRA8:25 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r1_fdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x"))) & (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: INTEGRA8:26 (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set   ($#k1_fdiff_1 :::"diff"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )  ")" ) ; 
 
theorem :: INTEGRA8:27 (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k19_sin_cos :::"cos"::: )  )) ; 
 
theorem :: INTEGRA8:28 (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ))) ; 
 
theorem :: INTEGRA8:29 (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k16_sin_cos :::"sin"::: )  )) ; 
 
theorem :: INTEGRA8:30 (Bool (Set (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_sin_cos2 :::"cosh"::: )  )) ; 
 
theorem :: INTEGRA8:31 (Bool (Set (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_sin_cos2 :::"sinh"::: )  )) ; 
 
theorem :: INTEGRA8:32 (Bool (Set (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k24_sin_cos :::"exp_R"::: )  )) ; 
 
theorem :: INTEGRA8:33 (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  ($#k29_sin_cos :::"tan"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k29_sin_cos :::"tan"::: )  )  ($#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  ($#k29_sin_cos :::"tan"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" )  ")" )) ; 
 
theorem :: INTEGRA8:34 (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  ($#k30_sin_cos :::"cot"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k30_sin_cos :::"cot"::: )  )  ($#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  ($#k30_sin_cos :::"cot"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )  ")" )) ; 
 
theorem :: INTEGRA8:35 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "r")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 definitionlet "r" be   ($#m1_subset_1 :::"Real":::); func  :::"Cst"::: "r" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: INTEGRA8:def 1 (Set (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k8_funcop_1 :::"-->"::: )  "r"); end; 





:: deftheorem    defines :::"Cst"::: INTEGRA8:def 1 :  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k1_integra8 :::"Cst"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "r"))))); 
 
theorem :: INTEGRA8:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "A")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_integra8 :::"Cst"::: )  (Num 1) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")))))) ; 
 
theorem :: INTEGRA8:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))) ; 
 begin  
theorem :: INTEGRA8:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k4_integra5 :::"integral"::: )   "(" (Set  "("  ($#k1_integra8 :::"Cst"::: )  (Num 1) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: INTEGRA8:39 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:40 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: INTEGRA8:41 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:42 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INTEGRA8:43 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:44 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: INTEGRA8:45 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:46 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:47 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INTEGRA8:48 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 2)))) ; 
 
theorem :: INTEGRA8:49 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INTEGRA8:50 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:51 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 2))))) ; 
 
theorem :: INTEGRA8:52 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:53 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:54 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k8_power :::"number_e"::: ) )  ($#k9_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INTEGRA8:55 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:56 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k8_power :::"number_e"::: ) )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" )))) ; 
 
theorem :: INTEGRA8:57 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:58 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k8_power :::"number_e"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" )))) ; 
 
theorem :: INTEGRA8:59 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k29_sin_cos :::"tan"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k29_sin_cos :::"tan"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (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 (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ))) & (Bool (Set (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k29_sin_cos :::"tan"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k29_sin_cos :::"tan"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:60 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k30_sin_cos :::"cot"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k30_sin_cos :::"cot"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (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   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))) & (Bool (Set (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k30_sin_cos :::"cot"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k30_sin_cos :::"cot"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:61 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k7_sin_cos2 :::"tanh"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k7_sin_cos2 :::"tanh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k7_sin_cos2 :::"tanh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:62 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k1_sin_cos6 :::"arcsin"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )))  ")" )  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k1_sin_cos6 :::"arcsin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k1_sin_cos6 :::"arcsin"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:63 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k4_sin_cos6 :::"arccos"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" )))  ")" )  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k4_sin_cos6 :::"arccos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k4_sin_cos6 :::"arccos"::: ) )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:64 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k1_sin_cos6 :::"arcsin"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )))  ")" )  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))))) ; 
 
theorem :: INTEGRA8:65 (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  ($#k4_sin_cos6 :::"arccos"::: ) )  ($#k2_fdiff_1 :::"`|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" )))  ")" )  ")" ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))))) ; 
 
theorem :: INTEGRA8:66 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:67 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "g"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:68 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))))) ; 
 
theorem :: INTEGRA8:69 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:70 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: INTEGRA8:71 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: INTEGRA8:72 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:73 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:74 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 2)))) ; 
 
theorem :: INTEGRA8:75 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:76 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:77 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k8_power :::"number_e"::: ) )  ($#k9_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INTEGRA8:78 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:79 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:80 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: INTEGRA8:81 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 3) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: INTEGRA8:82 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:83 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 2)))) ; 
 
theorem :: INTEGRA8:84 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set (Var "x")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA8:85 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:86 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:87 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  ($#k1_sin_cos2 :::"sinh"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:88 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:89 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: INTEGRA8:90 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:91 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: INTEGRA8:92 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:93 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: INTEGRA8:94 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k8_real_1 :::"*"::: )  (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INTEGRA8:95 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: INTEGRA8:96 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: INTEGRA8:97 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "A")) ")"  ")" )))) ; 
 
theorem :: INTEGRA8:98 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k1_sin_cos2 :::"sinh"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) ")" ) "," (Set (Var "A")) ")"  ")" )))) ; 
 
theorem :: INTEGRA8:99 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k1_sin_cos2 :::"sinh"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k4_sin_cos2 :::"cosh"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k4_sin_cos2 :::"cosh"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:100 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:101 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k3_valued_1 :::"+"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: INTEGRA8:102 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k47_valued_1 :::"-"::: )  (Set  ($#k16_sin_cos :::"sin"::: ) ) ")" ) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k19_sin_cos :::"cos"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))) ;