:: INTEGR1C  semantic presentation begin  


















definitionfunc  :::"R2-to-C":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: INTEGR1C:def 1 (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_xtuple_0 :::"`1"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k2_xtuple_0 :::"`2"::: )  ))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))))); end; 




:: deftheorem    defines :::"R2-to-C"::: INTEGR1C:def 1 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_integr1c :::"R2-to-C"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_xtuple_0 :::"`1"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k2_xtuple_0 :::"`2"::: )  ))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))))  ")" )); 
 definitionlet "a", "b" be   ($#m1_subset_1 :::"Real":::); let "x", "y" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); let "Z" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); func  :::"integral":::  "(" "f" "," "x" "," "y" "," "a" "," "b" "," "Z" ")"  ->   ($#m1_hidden :::"Complex":::) means :: INTEGR1C:def 2 (Bool  "ex" (Set (Var "u0")) "," (Set (Var "v0")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "u0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_comseq_3 :::"Re"::: )  "f" ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k1_integr1c :::"R2-to-C"::: ) ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  ($#k13_funct_3 :::"<:"::: ) "x" "," "y" ($#k13_funct_3 :::":>"::: ) ))) & (Bool (Set (Var "v0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_comseq_3 :::"Im"::: )  "f" ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k1_integr1c :::"R2-to-C"::: ) ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  ($#k13_funct_3 :::"<:"::: ) "x" "," "y" ($#k13_funct_3 :::":>"::: ) ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" "x"  ($#k2_fdiff_1 :::"`|"::: )  "Z" ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" "y"  ($#k2_fdiff_1 :::"`|"::: )  "Z" ")" ) ")" ) ")" ) "," "a" "," "b" ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" "x"  ($#k2_fdiff_1 :::"`|"::: )  "Z" ")" ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" "y"  ($#k2_fdiff_1 :::"`|"::: )  "Z" ")" ) ")" ) ")" ) "," "a" "," "b" ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))  ")" )); end; 










:: deftheorem    defines :::"integral"::: INTEGR1C:def 2 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "b7")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("  (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Z")) ")" )) "iff" (Bool  "ex" (Set (Var "u0")) "," (Set (Var "v0")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "u0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_comseq_3 :::"Re"::: )  (Set (Var "f")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k1_integr1c :::"R2-to-C"::: ) ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  ($#k13_funct_3 :::"<:"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k13_funct_3 :::":>"::: ) ))) & (Bool (Set (Var "v0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_comseq_3 :::"Im"::: )  (Set (Var "f")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  ($#k1_integr1c :::"R2-to-C"::: ) ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  ($#k13_funct_3 :::"<:"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k13_funct_3 :::":>"::: ) ))) & (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))  ")" ))  ")" )))))); 
 definitionlet "C" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); attr "C" is  :::"C1-curve-like":::  means :: INTEGR1C:def 3 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )(Bool  "ex" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "C")) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool "C"  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))  ")" )))); end; 




:: deftheorem    defines :::"C1-curve-like"::: INTEGR1C:def 3 :  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v1_integr1c :::"C1-curve-like"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )(Bool  "ex" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "C"))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))  ")" ))))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k2_numbers :::"COMPLEX"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_valued_0 :::"complex-valued"::: )     ($#v1_integr1c :::"C1-curve-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionmode C1-curve is   ($#v1_integr1c :::"C1-curve-like"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "C" be   ($#m1_subset_1 :::"C1-curve":::); assume 
(Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Const "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Const "f"))))
 ; func  :::"integral":::  "(" "f" "," "C" ")"  ->   ($#m1_hidden :::"Complex":::) means :: INTEGR1C:def 4 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )(Bool  "ex" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "C")) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool "C"  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_integr1c :::"integral"::: )   "(" "f" "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Z")) ")" ))  ")" )))); end; 







:: deftheorem    defines :::"integral"::: INTEGR1C:def 4 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"C1-curve":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "C")) ")" )) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )(Bool  "ex" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "C"))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Z")) ")" ))  ")" ))))  ")" )))); 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "C" be   ($#m1_subset_1 :::"C1-curve":::); pred "f" :::"is_integrable_on"::: "C" means :: INTEGR1C:def 5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "u0")) "," (Set (Var "v0")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "C")) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool "C"  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ))  ")" ))))); end; 





:: deftheorem    defines :::"is_integrable_on"::: INTEGR1C:def 5 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"C1-curve":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_integr1c :::"is_integrable_on"::: )  (Set (Var "C"))) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "u0")) "," (Set (Var "v0")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "C"))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ))  ")" )))))  ")" ))); 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "C" be   ($#m1_subset_1 :::"C1-curve":::); pred "f" :::"is_bounded_on"::: "C" means :: INTEGR1C:def 6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "u0")) "," (Set (Var "v0")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "C")) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool "C"  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" ))))); end; 





:: deftheorem    defines :::"is_bounded_on"::: INTEGR1C:def 6 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"C1-curve":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_integr1c :::"is_bounded_on"::: )  (Set (Var "C"))) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "u0")) "," (Set (Var "v0")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "x")))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "y")))) & (Bool (Set (Var "Z")) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "x"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "C"))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "v0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "x"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "u0"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "y"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" ) ")" ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" )))))  ")" ))); 
 begin  
theorem :: INTEGR1C:1 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"C1-curve":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r1_integr1c :::"is_integrable_on"::: )  (Set (Var "C"))) & (Bool (Set (Var "g"))  ($#r1_integr1c :::"is_integrable_on"::: )  (Set (Var "C"))) & (Bool (Set (Var "f"))  ($#r2_integr1c :::"is_bounded_on"::: )  (Set (Var "C"))) & (Bool (Set (Var "g"))  ($#r2_integr1c :::"is_bounded_on"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k3_integr1c :::"integral"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "g")) ")" ) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "C")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "g")) "," (Set (Var "C")) ")"  ")" ))))) ; 
 
theorem :: INTEGR1C:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"C1-curve":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_integr1c :::"is_integrable_on"::: )  (Set (Var "C"))) & (Bool (Set (Var "f"))  ($#r2_integr1c :::"is_bounded_on"::: )  (Set (Var "C")))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k3_integr1c :::"integral"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "C")) ")"  ")" )))))) ; 
 begin  
theorem :: INTEGR1C:3 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_subset_1 :::"C1-curve":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_integr1c :::"is_integrable_on"::: )  (Set (Var "C"))) & (Bool (Set (Var "f"))  ($#r2_integr1c :::"is_bounded_on"::: )  (Set (Var "C"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "d")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "d")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C1"))))) "holds"  (Bool (Set (Set (Var "C"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t"))))  ")" ) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "C2"))))) "holds"  (Bool (Set (Set (Var "C"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "t"))))  ")" )) "holds"  (Bool (Set   ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "C1")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k3_integr1c :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "C2")) ")"  ")" )))))) ;