:: CFDIFF_1  semantic presentation begin  













































definitionlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "IT" be   ($#m1_subset_1 :::"Complex_Sequence":::); attr "IT" is "x" :::"-convergent":::  means :: CFDIFF_1:def 1 (Bool  "("  (Bool "IT" "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  "IT")  ($#r1_hidden :::"="::: )  "x")  ")" ); end; 





:: deftheorem    defines :::"-convergent"::: CFDIFF_1:def 1 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is" (Set (Var "x"))  ($#v1_cfdiff_1 :::"-convergent"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")" ))); 
 
theorem :: CFDIFF_1:1 (Bool  "for" (Set (Var "rs")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "cs")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "rs"))  ($#r1_funct_2 :::"="::: )  (Set (Var "cs"))) & (Bool (Set (Var "rs")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Var "cs")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ))) ; 
 definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"InvShift"::: "r" ->   ($#m1_subset_1 :::"Complex_Sequence":::) means :: CFDIFF_1:def 2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k7_real_1 :::"+"::: )  "r" ")" )))); end; 





:: deftheorem    defines :::"InvShift"::: CFDIFF_1:def 2 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cfdiff_1 :::"InvShift"::: )  (Set (Var "r")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ))))  ")" ))); 
 
theorem :: CFDIFF_1:2 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k1_cfdiff_1 :::"InvShift"::: )  (Set (Var "r"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_cfdiff_1 :::"InvShift"::: )  "r") ->   ($#v2_comseq_2 :::"convergent"::: )   ; 
end; 
theorem :: CFDIFF_1:3 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "("  ($#k1_cfdiff_1 :::"InvShift"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_cfdiff_1 :::"InvShift"::: )  "r") ->   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )   ; 
end; registration
cluster bbbadV1_RELAT_1()   ($#v2_relat_1 :::"non-zero"::: )   bbbadV4_RELAT_1((Set   ($#k5_numbers :::"NAT"::: )  )) bbbadV5_RELAT_1((Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_XBOOLE_0()   ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_valued_0 :::"complex-valued"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; registration
cluster   ($#v2_relat_1 :::"non-zero"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    ->   ($#v2_comseq_2 :::"convergent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; registration
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k5_numbers :::"NAT"::: )  )) bbbadV5_RELAT_1((Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )     ($#v3_funct_1 :::"constant"::: )   bbbadV1_XBOOLE_0()   ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_valued_0 :::"complex-valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; 
theorem :: CFDIFF_1:4 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")))))  ")" )) ; 
 
theorem :: CFDIFF_1:5 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "Nseq")) "being" bbbadV5_VALUED_0()  ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k9_comseq_3 :::"*"::: )  (Set (Var "Nseq")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "Nseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))))) ; 
 





definitionlet "IT" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); attr "IT" is  :::"RestFunc-like":::  means :: CFDIFF_1:def 3 (Bool  "for" (Set (Var "h")) "being"   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" "IT"  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" )) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" "IT"  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); end; 




:: deftheorem    defines :::"RestFunc-like"::: CFDIFF_1:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_cfdiff_1 :::"RestFunc-like"::: )  ) "iff" (Bool  "for" (Set (Var "h")) "being"   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "IT"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" )) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "IT"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))  ")" )); 
 registration
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k2_numbers :::"COMPLEX"::: )  )) bbbadV5_RELAT_1((Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; definitionmode C_RestFunc is   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "IT" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); attr "IT" is  :::"linear":::  means :: CFDIFF_1:def 4 (Bool  "ex" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set "IT"  ($#k7_partfun1 :::"/."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_complex1 :::"*"::: )  (Set (Var "z")))))); end; 




:: deftheorem    defines :::"linear"::: CFDIFF_1:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_cfdiff_1 :::"linear"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "IT"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_complex1 :::"*"::: )  (Set (Var "z"))))))  ")" )); 
 registration
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k2_numbers :::"COMPLEX"::: )  )) bbbadV5_RELAT_1((Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_valued_0 :::"complex-valued"::: )     ($#v3_cfdiff_1 :::"linear"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; definitionmode C_LinearFunc is   ($#v1_partfun1 :::"total"::: )     ($#v3_cfdiff_1 :::"linear"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; 









registrationlet "L1", "L2" be   ($#m1_subset_1 :::"C_LinearFunc":::); 
cluster (Set "L1"  ($#k1_valued_1 :::"+"::: )  "L2") ->   ($#v1_partfun1 :::"total"::: )     ($#v3_cfdiff_1 :::"linear"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 

cluster (Set "L1"  ($#k45_valued_1 :::"-"::: )  "L2") ->   ($#v1_partfun1 :::"total"::: )     ($#v3_cfdiff_1 :::"linear"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
end; registrationlet "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); let "L" be   ($#m1_subset_1 :::"C_LinearFunc":::); 
cluster (Set "a"  ($#k24_valued_1 :::"(#)"::: )  "L") ->   ($#v1_partfun1 :::"total"::: )     ($#v3_cfdiff_1 :::"linear"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
end; registrationlet "R1", "R2" be   ($#m1_subset_1 :::"C_RestFunc":::); 
cluster (Set "R1"  ($#k1_valued_1 :::"+"::: )  "R2") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 

cluster (Set "R1"  ($#k45_valued_1 :::"-"::: )  "R2") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 

cluster (Set "R1"  ($#k18_valued_1 :::"(#)"::: )  "R2") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
end; registrationlet "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); let "R" be   ($#m1_subset_1 :::"C_RestFunc":::); 
cluster (Set "a"  ($#k24_valued_1 :::"(#)"::: )  "R") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
end; registrationlet "L1", "L2" be   ($#m1_subset_1 :::"C_LinearFunc":::); 
cluster (Set "L1"  ($#k18_valued_1 :::"(#)"::: )  "L2") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
end; registrationlet "R" be   ($#m1_subset_1 :::"C_RestFunc":::); let "L" be   ($#m1_subset_1 :::"C_LinearFunc":::); 
cluster (Set "R"  ($#k18_valued_1 :::"(#)"::: )  "L") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 

cluster (Set "L"  ($#k18_valued_1 :::"(#)"::: )  "R") ->   ($#v1_partfun1 :::"total"::: )     ($#v2_cfdiff_1 :::"RestFunc-like"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
end; definitionlet "z0" be   ($#m1_hidden :::"Complex":::); mode  :::"Neighbourhood":::  "of" "z0" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: CFDIFF_1:def 5 (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g"))) & (Bool  "{"  (Set (Var "y")) where y "is"   ($#m1_hidden :::"Complex":::) : (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k6_xcmplx_0 :::"-"::: )  "z0" ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))  "}"    ($#r1_tarski :::"c="::: )  it)  ")" )); end; 





:: deftheorem    defines :::"Neighbourhood"::: CFDIFF_1:def 5 :  (Bool  "for" (Set (Var "z0")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0"))) "iff" (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g"))) & (Bool  "{"  (Set (Var "y")) where y "is"   ($#m1_hidden :::"Complex":::) : (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))  "}"    ($#r1_tarski :::"c="::: )  (Set (Var "b2")))  ")" ))  ")" ))); 
 
theorem :: CFDIFF_1:6 (Bool  "for" (Set (Var "z0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "g")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))) "holds"  (Bool  "{"  (Set (Var "y")) where y "is"   ($#m1_hidden :::"Complex":::) : (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))  "}"   "is"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0"))))) ; 
 
theorem :: CFDIFF_1:7 (Bool  "for" (Set (Var "z0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0")) "holds"  (Bool (Set (Var "z0"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))))) ; 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "z0" be   ($#m1_hidden :::"Complex":::); pred "f" :::"is_differentiable_in"::: "z0" means :: CFDIFF_1:def 6 (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" "z0" "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"C_LinearFunc":::)(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"C_RestFunc":::) "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "z")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "z0" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  "z0" ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  "z0" ")" ) ")" ))))))  ")" )); end; 





:: deftheorem    defines :::"is_differentiable_in"::: CFDIFF_1: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 "z0")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "z0"))) "iff" (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"C_LinearFunc":::)(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"C_RestFunc":::) "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "z")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "z0")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ")" ))))))  ")" ))  ")" ))); 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "z0" be   ($#m1_hidden :::"Complex":::); assume 
(Bool (Set (Const "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Const "z0")))
 ; func  :::"diff":::  "(" "f" "," "z0" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) means :: CFDIFF_1:def 7 (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" "z0" "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"C_LinearFunc":::)(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"C_RestFunc":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k10_funct_2 :::"/."::: )  (Set  ($#k6_complex1 :::"1r"::: ) ))) & (Bool  "("   "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "z")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "z0" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  "z0" ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  "z0" ")" ) ")" )))  ")" )  ")" )))  ")" )); end; 







:: deftheorem    defines :::"diff"::: CFDIFF_1:def 7 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "z0")) "being"   ($#m1_hidden :::"Complex":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "z0")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "z0")) ")" )) "iff" (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"C_LinearFunc":::)(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"C_RestFunc":::) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k10_funct_2 :::"/."::: )  (Set  ($#k6_complex1 :::"1r"::: ) ))) & (Bool  "("   "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "z")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "z0")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k10_funct_2 :::"/."::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ")" )))  ")" )  ")" )))  ")" ))  ")" )))); 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); attr "f" is  :::"differentiable":::  means :: CFDIFF_1:def 8 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f"))) "holds"  (Bool "f"  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x")))); end; 




:: deftheorem    defines :::"differentiable"::: CFDIFF_1:def 8 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v4_cfdiff_1 :::"differentiable"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x"))))  ")" )); 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "X" be    ($#m1_hidden :::"set"::: )  ; pred "f" :::"is_differentiable_on"::: "X" means :: CFDIFF_1:def 9 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool (Set "f"  ($#k5_relset_1 :::"|"::: )  "X") "is"   ($#v4_cfdiff_1 :::"differentiable"::: )  )  ")" ); end; 





:: deftheorem    defines :::"is_differentiable_on"::: CFDIFF_1:def 9 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v4_cfdiff_1 :::"differentiable"::: )  )  ")" )  ")" ))); 
 
theorem :: CFDIFF_1:8 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )))) ; 
 definitionlet "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); attr "X" is  :::"closed":::  means :: CFDIFF_1:def 10 (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s1")))  ($#r1_tarski :::"c="::: )  "X") & (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r2_hidden :::"in"::: )  "X")); end; 




:: deftheorem    defines :::"closed"::: CFDIFF_1:def 10 :  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v5_cfdiff_1 :::"closed"::: )  ) "iff" (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s1")))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" )); 
 definitionlet "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); attr "X" is  :::"open":::  means :: CFDIFF_1:def 11 (Bool (Set "X"  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v5_cfdiff_1 :::"closed"::: )  ); end; 




:: deftheorem    defines :::"open"::: CFDIFF_1:def 11 :  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v6_cfdiff_1 :::"open"::: )  ) "iff" (Bool (Set (Set (Var "X"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v5_cfdiff_1 :::"closed"::: )  )  ")" )); 
 
theorem :: CFDIFF_1:9 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v6_cfdiff_1 :::"open"::: )  )) "holds"  (Bool  "for" (Set (Var "z0")) "being"   ($#m1_hidden :::"Complex":::)  "st" (Bool (Bool (Set (Var "z0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0")) "st" (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))))) ; 
 
theorem :: CFDIFF_1:10 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v6_cfdiff_1 :::"open"::: )  )) "holds"  (Bool  "for" (Set (Var "z0")) "being"   ($#m1_hidden :::"Complex":::)  "st" (Bool (Bool (Set (Var "z0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool  "{"  (Set (Var "y")) where y "is"   ($#m1_hidden :::"Complex":::) : (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))  "}"    ($#r1_tarski :::"c="::: )  (Set (Var "X")))))) ; 
 
theorem :: CFDIFF_1:11 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "z0")) "being"   ($#m1_hidden :::"Complex":::)  "st" (Bool (Bool (Set (Var "z0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "z0")) "st" (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))))  ")" )) "holds"  (Bool (Set (Var "X")) "is"   ($#v6_cfdiff_1 :::"open"::: )  )) ; 
 
theorem :: CFDIFF_1:12 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v6_cfdiff_1 :::"open"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"Complex":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))))  ")" )) ; 
 
theorem :: CFDIFF_1:13 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "z0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "y")) where y "is"   ($#m1_hidden :::"Complex":::) : (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  "}"  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v6_cfdiff_1 :::"open"::: )  )))) ; 
 
theorem :: CFDIFF_1:14 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "z0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "y")) where y "is"   ($#m1_hidden :::"Complex":::) : (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z0")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  "}"  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v5_cfdiff_1 :::"closed"::: )  )))) ; 
 registration
cluster bbbadV1_MEMBERED()   ($#v6_cfdiff_1 :::"open"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k2_numbers :::"COMPLEX"::: ) ))); 
end; 



theorem :: CFDIFF_1:15 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) "iff" (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x")))  ")" )  ")" )  ")" ))) ; 
 
theorem :: CFDIFF_1:16 (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y")) "is"   ($#v6_cfdiff_1 :::"open"::: )  ))) ; 
 definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); let "X" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Const "X")))
 ; func "f" :::"`|"::: "X" ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: CFDIFF_1:def 12 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" "f" "," (Set (Var "x")) ")" ))  ")" )  ")" ); end; 







:: deftheorem    defines :::"`|"::: CFDIFF_1:def 12 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))  ")" )  ")" )  ")" )))); 
 
theorem :: CFDIFF_1:17 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "ex" (Set (Var "a1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st" (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a1")) ($#k1_tarski :::"}"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )  ")" ))) ; 
 registrationlet "seq" be   ($#v2_relat_1 :::"non-zero"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); let "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "seq"  ($#k9_nat_1 :::"^\"::: )  "k") ->   ($#v2_relat_1 :::"non-zero"::: )   ; 
end; registrationlet "h" be   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); let "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set "h"  ($#k9_nat_1 :::"^\"::: )  "n") -> (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: CFDIFF_1:18 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "seq1")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k2_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: CFDIFF_1:19 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq1")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k46_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: CFDIFF_1:20 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k36_valued_1 :::"""::: )  )))) ; 
 
theorem :: CFDIFF_1:21 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: CFDIFF_1:22 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "N")) "being"    ($#m1_cfdiff_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_cfdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v3_funct_1 :::"constant"::: )    ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "h"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "N")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set  "(" (Set (Var "h"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "c")) ")" ) ")" )  ($#k46_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "c")) ")" ) ")" )) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set  "(" (Set (Var "h"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "c")) ")" ) ")" )  ($#k46_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "c")) ")" ) ")" ) ")" )))  ")" )))))) ; 
 
theorem :: CFDIFF_1:23 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "f2"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "f2")))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x0")) ")"  ")" )))  ")" ))) ; 
 
theorem :: CFDIFF_1:24 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "f2"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "f2")))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" )  ($#k11_complex1 :::"-"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x0")) ")"  ")" )))  ")" ))) ; 
 
theorem :: CFDIFF_1:25 (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")"  ")" )))  ")" )))) ; 
 
theorem :: CFDIFF_1:26 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "f2"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "f2")))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" )  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" )  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x0")) ")"  ")" ) ")" )))  ")" ))) ; 
 
theorem :: CFDIFF_1:27 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "Z"))))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_complex1 :::"1r"::: )  ))  ")" )  ")" ))) ; 
 
theorem :: CFDIFF_1:28 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "f2"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "f2")))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")"  ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" ))) ; 
 
theorem :: CFDIFF_1:29 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "f2"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "f2")))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")"  ")" )  ($#k11_complex1 :::"-"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" ))) ; 
 
theorem :: CFDIFF_1:30 (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "a"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: CFDIFF_1:31 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "f2"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "f2")))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")"  ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k2_cfdiff_1 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x")) ")"  ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: CFDIFF_1:32 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "Z"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )  ")" ))) ; 
 
theorem :: CFDIFF_1:33 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_complex1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k8_complex1 :::"+"::: )  (Set (Var "b"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_cfdiff_1 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )  ")" )))) ; 
 
theorem :: CFDIFF_1:34 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool (Set (Var "f"))  ($#r1_cfcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))))) ; 
 
theorem :: CFDIFF_1:35 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r2_cfcont_1 :::"is_continuous_on"::: )  (Set (Var "X"))))) ; 
 
theorem :: CFDIFF_1:36 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "Z")) "being"   ($#v6_cfdiff_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r2_cfdiff_1 :::"is_differentiable_on"::: )  (Set (Var "Z")))))) ; 
 
theorem :: CFDIFF_1:37 canceled; 
 
theorem :: CFDIFF_1:38 (Bool  "for" (Set (Var "x0")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_cfdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"C_RestFunc":::) "st"  (Bool  "("  (Bool (Set (Set (Var "R"))  ($#k10_funct_2 :::"/."::: )  (Set  ($#k5_complex1 :::"0c"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "R"))  ($#r1_cfcont_1 :::"is_continuous_in"::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )))) ;