:: PDIFF_9  semantic presentation begin  












theorem :: PDIFF_9:1 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))))) ; 
 
theorem :: PDIFF_9:2 (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_nfcont_1 :::"is_continuous_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 "s1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s1")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "s1")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set (Var "s1")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "s1"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "s1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "s1")) ")" )))  ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:3 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))))) ; 
 
theorem :: PDIFF_9:4 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "Z")))))) ; 
 
theorem :: PDIFF_9:5 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: PDIFF_9:6 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "i")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))  ")" )))) ; 
 
theorem :: PDIFF_9:7 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )  ($#k7_integr15 :::"+"::: )  (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "g")) ")" ))) & (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )  ($#k8_integr15 :::"-"::: )  (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "g")) ")" )))  ")" ))) ; 
 
theorem :: PDIFF_9:8 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "r"))  ($#k9_integr15 :::"(#)"::: )  (Set  "("  ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: PDIFF_9:9 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) )  ($#r2_relset_1 :::"="::: )  (Set  ($#k1_nfcont_4 :::"|."::: ) (Set (Var "g")) ($#k1_nfcont_4 :::".|"::: ) ))))) ; 
 
theorem :: PDIFF_9:10 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) "iff" (Bool (Set (Var "Y")) "is"   ($#v3_nfcont_1 :::"open"::: )  )  ")" )))) ; 
 
theorem :: PDIFF_9:11 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "("  ($#k6_pdiff_1 :::"reproj"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "j")) ")" ) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "q")) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: PDIFF_9:12 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "j"))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_pdiff_1 :::"reproj"::: )   "(" (Set (Var "i")) "," (Set (Var "x")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))) ; 
 begin  
theorem :: PDIFF_9:13 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  )))) ; 
 
theorem :: PDIFF_9:14 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r1_pdiff_1 :::"is_differentiable_in"::: )  (Set (Var "x")))  ")" )  ")" )  ")" )))) ; 
 definitionlet "m", "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "n")) ")" ); assume 
(Bool (Set (Const "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Const "f"))))
 ; func "f" :::"`|"::: "Z" ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  "n" ")" ) ")"  ")" ) means :: PDIFF_9:def 1 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "Z") & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  "m")  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Z")) "holds"  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_pdiff_1 :::"diff"::: )   "(" "f" "," (Set (Var "x")) ")" ))  ")" )  ")" ); end; 









:: deftheorem    defines :::"`|"::: PDIFF_9:def 1 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" ) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_pdiff_9 :::"`|"::: )  (Set (Var "Z")))) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b5")))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "b5"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))  ")" )  ")" )  ")" ))))); 
 
theorem :: PDIFF_9:15 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_integr15 :::"+"::: )  (Set (Var "g")))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k7_integr15 :::"+"::: )  (Set (Var "g")) ")" )  ($#k1_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )  ($#k7_integr15 :::"+"::: )  (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:16 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_integr15 :::"-"::: )  (Set (Var "g")))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k8_integr15 :::"-"::: )  (Set (Var "g")) ")" )  ($#k1_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )  ($#k8_integr15 :::"-"::: )  (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:17 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k9_integr15 :::"(#)"::: )  (Set (Var "f")))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "r"))  ($#k9_integr15 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k1_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k9_integr15 :::"(#)"::: )  (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" ))))) ; 
 
theorem :: PDIFF_9:18 (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "j")) ")" ) ")"  ")" ) (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "j")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")))))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "p")) ($#k1_normsp_0 :::".||"::: ) )  ($#k11_binop_2 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:19 (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "j")) ")" ) ")"  ")" ) (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "j")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "p")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) ))  ")" )))) ; 
 
theorem :: PDIFF_9:20 (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "j")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) )  ($#k11_binop_2 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))))) ; 
 
theorem :: PDIFF_9:21 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "f"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k12_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "g")) "," (Set (Var "y")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))))))))))) ; 
 
theorem :: PDIFF_9:22 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "f"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "for" (Set (Var "x0")) "," (Set (Var "x1")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "y0")) "," (Set (Var "y1")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "x0"))  ($#r1_hidden :::"="::: )  (Set (Var "y0"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x1")) ")" )  ($#k8_euclid :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" ) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "g"))  ($#k15_pdiff_1 :::"`partial|"::: )   "(" (Set (Var "Y")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "y1")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k15_pdiff_1 :::"`partial|"::: )   "(" (Set (Var "Y")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "y0")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) )))))))))) ; 
 
theorem :: PDIFF_9:23 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "g"))  ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: )  (Set (Var "Y")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "g"))  ($#k15_pdiff_1 :::"`partial|"::: )   "(" (Set (Var "Y")) "," (Set (Var "i")) ")" )  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "Y")))  ")" )  ")" ))))))) ; 
 
theorem :: PDIFF_9:24 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )  ")" ) "iff" (Bool  "("  (Bool (Set (Var "g"))  ($#r2_ndiff_1 :::"is_differentiable_on"::: )  (Set (Var "Y"))) & (Bool (Set (Set (Var "g"))  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "Y")))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "Y")))  ")" )  ")" )))))) ; 
 
theorem :: PDIFF_9:25 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set (Var "g"))  ($#r2_ndiff_1 :::"is_differentiable_on"::: )  (Set (Var "Y"))) & (Bool (Set (Set (Var "g"))  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "Y")))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "x1"))  ($#k8_euclid :::"-"::: )  (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m"))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x1")) ")"  ")" )  ($#k1_pdiff_6 :::"."::: )  (Set (Var "v")) ")" )  ($#k8_euclid :::"-"::: )  (Set  "(" (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")"  ")" )  ($#k1_pdiff_6 :::"."::: )  (Set (Var "v")) ")" ) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "v")) ($#k12_euclid :::".|"::: ) ))))  ")" )  ")" )))  ")" )  ")" )  ")" )))))) ; 
 
theorem :: PDIFF_9:26 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )  ")" ) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "x1"))  ($#k8_euclid :::"-"::: )  (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m"))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x1")) ")"  ")" )  ($#k1_pdiff_6 :::"."::: )  (Set (Var "v")) ")" )  ($#k8_euclid :::"-"::: )  (Set  "(" (Set  "("  ($#k8_pdiff_1 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")"  ")" )  ($#k1_pdiff_6 :::"."::: )  (Set (Var "v")) ")" ) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "v")) ($#k12_euclid :::".|"::: ) ))))  ")" )  ")" )))  ")" )  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:27 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_pdiff_9 :::"`|"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "Z")))))))) ; 
 
theorem :: PDIFF_9:28 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )  ")" ) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "g"))  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "Y")))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "Y")))  ")" )  ")" )))))) ; 
 
theorem :: PDIFF_9:29 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x"))) & (Bool (Set (Var "g"))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_integr15 :::"+"::: )  (Set (Var "g")))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "f"))  ($#k8_integr15 :::"-"::: )  (Set (Var "g")))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x")))  ")" )))) ; 
 
theorem :: PDIFF_9:30 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k9_integr15 :::"(#)"::: )  (Set (Var "f")))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x"))))))) ; 
 
theorem :: PDIFF_9:31 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x")))) "holds"  (Bool (Set   ($#k2_nfcont_4 :::"-"::: )  (Set (Var "f")))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x")))))) ; 
 
theorem :: PDIFF_9:32 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x")))) "holds"  (Bool (Set  ($#k1_nfcont_4 :::"|."::: ) (Set (Var "f")) ($#k1_nfcont_4 :::".|"::: ) )  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x")))))) ; 
 
theorem :: PDIFF_9:33 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "g"))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_integr15 :::"+"::: )  (Set (Var "g")))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "f"))  ($#k8_integr15 :::"-"::: )  (Set (Var "g")))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" )))) ; 
 
theorem :: PDIFF_9:34 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k9_integr15 :::"(#)"::: )  (Set (Var "f")))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: PDIFF_9:35 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))) "holds"  (Bool (Set   ($#k2_nfcont_4 :::"-"::: )  (Set (Var "f")))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))))) ; 
 
theorem :: PDIFF_9:36 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "i"))) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0"))) "iff" (Bool  "("  (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "i")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k8_euclid :::"-"::: )  (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))  ")" )  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:37 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m"))) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0"))) "iff" (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r3_pdiff_7 :::"is_continuous_in"::: )  (Set (Var "x0")))  ")" )))) ; 
 
theorem :: PDIFF_9:38 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "g"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0")))  ")" )))) ; 
 
theorem :: PDIFF_9:39 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0"))))))) ; 
 
theorem :: PDIFF_9:40 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0")))) "holds"  (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) )  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0")))))) ; 
 
theorem :: PDIFF_9:41 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "i")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "i")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x"))) & (Bool (Set (Var "g"))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x")))))) ; 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_continuous_on"::: "Z" means :: PDIFF_9:def 2 (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  "m")  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  "Z")) "holds"  (Bool (Set "f"  ($#k2_partfun1 :::"|"::: )  "Z")  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0")))); end; 






:: deftheorem    defines :::"is_continuous_on"::: PDIFF_9:def 2 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) "iff" (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z")))  ($#r2_nfcont_4 :::"is_continuous_in"::: )  (Set (Var "x0"))))  ")" )))); 
 
theorem :: PDIFF_9:42 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" ) "iff" (Bool (Set (Var "g"))  ($#r4_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" ))))) ; 
 
theorem :: PDIFF_9:43 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "s")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set (Var "s")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "g"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "s"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "g"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "s")) ")" )))  ")" ))  ")" ))))) ; 
 
theorem :: PDIFF_9:44 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" ) "iff" (Bool (Set (Var "g"))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" ))))) ; 
 
theorem :: PDIFF_9:45 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) "iff" (Bool  "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "x1"))  ($#k8_euclid :::"-"::: )  (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x1")) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))))  ")" )))) ; 
 
theorem :: PDIFF_9:46 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "g"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" )))) ; 
 
theorem :: PDIFF_9:47 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: PDIFF_9:48 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "g"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))))) ; 
 
theorem :: PDIFF_9:49 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" ) "iff" (Bool (Set (Var "g"))  ($#r4_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "Z")))  ")" ))))) ; 
 
theorem :: PDIFF_9:50 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "Z")))) "holds"  (Bool (Set  ($#k1_nfcont_4 :::"|."::: ) (Set (Var "f")) ($#k1_nfcont_4 :::".|"::: ) )  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "Z")))))) ; 
 
theorem :: PDIFF_9:51 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x"))) & (Bool (Set (Var "g"))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x"))) & (Bool (Set   ($#k1_pdiff_7 :::"diff"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) ")"  ")" ))) & (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x"))) & (Bool (Set   ($#k1_pdiff_7 :::"diff"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) ")"  ")" )))  ")" )))) ; 
 
theorem :: PDIFF_9:52 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x"))) & (Bool (Set   ($#k1_pdiff_7 :::"diff"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )))  ")" ))))) ; 
 definitionlet "Z" be    ($#m1_hidden :::"set"::: )  ; let "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_differentiable_on"::: "Z" means :: PDIFF_9:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  "m")  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Z")) "holds"  (Bool (Set "f"  ($#k2_partfun1 :::"|"::: )  "Z")  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x")))); end; 






:: deftheorem    defines :::"is_differentiable_on"::: PDIFF_9:def 3 :  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "Z"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z")))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x"))))  ")" )))); 
 
theorem :: PDIFF_9:53 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "Z")))  ")" ) "iff" (Bool (Set (Var "g"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "Z")))  ")" ))))) ; 
 
theorem :: PDIFF_9:54 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r1_pdiff_7 :::"is_differentiable_in"::: )  (Set (Var "x"))))  ")" )))) ; 
 
theorem :: PDIFF_9:55 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  )))) ; 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); assume 
(Bool (Set (Const "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Const "f"))))
 ; func "f" :::"`|"::: "Z" ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ")"  ")" ) means :: PDIFF_9:def 4 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "Z") & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  "m")  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Z")) "holds"  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_pdiff_7 :::"diff"::: )   "(" "f" "," (Set (Var "x")) ")" ))  ")" )  ")" ); end; 








:: deftheorem    defines :::"`|"::: PDIFF_9:def 4 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "Z")))) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))  ")" )  ")" )  ")" ))))); 
 
theorem :: PDIFF_9:56 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Var "g"))  ($#r1_pdiff_6 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k1_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )))  ")" )  ")" ))))) ; 
 
theorem :: PDIFF_9:57 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:58 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" )  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:59 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_pdiff_9 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )))  ")" )  ")" ))))) ; 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "i" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_partial_differentiable_on"::: "Z" "," "i" means :: PDIFF_9:def 5 (Bool  "("  (Bool "Z"  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  "m")  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Z")) "holds"  (Bool (Set "f"  ($#k2_partfun1 :::"|"::: )  "Z")  ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: )  (Set (Var "x")) "," "i")  ")" )  ")" ); end; 







:: deftheorem    defines :::"is_partial_differentiable_on"::: PDIFF_9:def 5 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "i"))) "iff" (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z")))  ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: )  (Set (Var "x")) "," (Set (Var "i")))  ")" )  ")" )  ")" ))))); 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "i" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); assume 
(Bool (Set (Const "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Const "Z")) "," (Set (Const "i")))
 ; func "f" :::"`partial|":::  "(" "Z" "," "i" ")"  ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_9:def 6 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "Z") & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  "m")  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Z")) "holds"  (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_pdiff_1 :::"partdiff"::: )   "(" "f" "," (Set (Var "x")) "," "i" ")" ))  ")" )  ")" ); end; 









:: deftheorem    defines :::"`partial|"::: PDIFF_9:def 6 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "i")))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set (Var "i")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b5")))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "b5"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ))  ")" )  ")" )  ")" )))))); 
 
theorem :: PDIFF_9:60 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: )  (Set (Var "x")) "," (Set (Var "i")))  ")" )  ")" )  ")" ))))) ; 
 
theorem :: PDIFF_9:61 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) "iff" (Bool (Set (Var "g"))  ($#r2_pdiff_7 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))  ")" )))))) ; 
 
theorem :: PDIFF_9:62 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k1_euclid :::"REAL"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set   ($#k3_pdiff_1 :::"<>*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "g"))  ($#k2_pdiff_7 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r4_pdiff_7 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )))))) ; 
 
theorem :: PDIFF_9:63 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r1_pdiff_9 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )  ")" ) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_pdiff_9 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x0")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x0"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "x1"))  ($#k8_euclid :::"-"::: )  (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m"))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x1")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "v")) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_pdiff_7 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "v")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "v")) ($#k12_euclid :::".|"::: ) ))))  ")" )  ")" )))  ")" )  ")" )  ")" )))) ; 
 
theorem :: PDIFF_9:64 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "f"))  ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: )  (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set (Var "g"))  ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: )  (Set (Var "x")) "," (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")))  ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: )  (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set   ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" ) ")" )))  ")" ))))) ; 
 
theorem :: PDIFF_9:65 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Var "g"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )))  ")" )  ")" ))))) ; 
 
theorem :: PDIFF_9:66 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Var "g"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )))  ")" )  ")" ))))) ; 
 
theorem :: PDIFF_9:67 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )))  ")" )  ")" )))))) ; 
 
theorem :: PDIFF_9:68 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Var "g"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "m")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k11_pdiff_1 :::"partdiff"::: )   "(" (Set (Var "g")) "," (Set (Var "x")) "," (Set (Var "i")) ")"  ")" ) ")" )))  ")" )  ")" ))))) ; 
 begin  definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "I" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"PartDiffSeq":::  "(" "f" "," "Z" "," "I" ")"  ->   ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_9:def 7 (Bool  "("  (Bool (Set it  ($#k1_seqfunc :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_relset_1 :::"="::: )  "f") & (Bool  "("   "for" (Set (Var "i")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set it  ($#k1_seqfunc :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" it  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" "Z" "," (Set  "(" "I"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))  ")" )  ")" ); end; 








:: deftheorem    defines :::"PartDiffSeq"::: PDIFF_9:def 7 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "I")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "I")) ")" )) "iff" (Bool  "("  (Bool (Set (Set (Var "b5"))  ($#k1_seqfunc :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_relset_1 :::"="::: )  (Set (Var "f"))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_seqfunc :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "b5"))  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set  "(" (Set (Var "I"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))  ")" )  ")" )  ")" )))))); 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "I" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_partial_differentiable_on"::: "Z" "," "I" means :: PDIFF_9:def 8 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  "I" ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" "f" "," "Z" "," "I" ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  "Z" "," (Set "I"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )))); end; 







:: deftheorem    defines :::"is_partial_differentiable_on"::: PDIFF_9:def 8 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "I")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "I"))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Set (Var "I"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))))  ")" ))))); 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; let "I" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); func "f" :::"`partial|":::  "(" "Z" "," "I" ")"  ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  "m" ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: PDIFF_9:def 9 (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" "f" "," "Z" "," "I" ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  "I" ")" )); end; 








:: deftheorem    defines :::"`partial|"::: PDIFF_9:def 9 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "I")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set (Var "I")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")) ")" ))))))); 
 
theorem :: PDIFF_9:69 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Var "g"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" ) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Set (Var "I"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" ) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )))  ")" )))))) ; 
 
theorem :: PDIFF_9:70 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Var "g"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )))  ")" ))))) ; 
 
theorem :: PDIFF_9:71 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Var "g"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" ) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Set (Var "I"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" ) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )))  ")" )))))) ; 
 
theorem :: PDIFF_9:72 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Var "g"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")) ")" )  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )))  ")" ))))) ; 
 
theorem :: PDIFF_9:73 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")) ")" )  ($#k21_binop_2 :::"-"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Set (Var "I"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k4_pdiff_9 :::"PartDiffSeq"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )  ($#k1_seqfunc :::"."::: )  (Set (Var "i")) ")" )))  ")" ))))))) ; 
 
theorem :: PDIFF_9:74 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "I"))) & (Bool (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "I")) ")"  ")" )))  ")" )))))) ; 
 definitionlet "m" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Const "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); let "k" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "Z" be    ($#m1_hidden :::"set"::: )  ; pred "f" :::"is_partial_differentiable_up_to_order"::: "k" "," "Z" means :: PDIFF_9:def 10 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")))  ($#r1_xxreal_0 :::"<="::: )  "k") & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  "m"))) "holds"  (Bool "f"  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  "Z" "," (Set (Var "I")))); end; 







:: deftheorem    defines :::"is_partial_differentiable_up_to_order"::: PDIFF_9:def 10 :  (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "k")) "," (Set (Var "Z"))) "iff" (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "I"))))  ")" ))))); 
 
theorem :: PDIFF_9:75 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "I")) "," (Set (Var "G")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Set (Var "G"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "I")))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "G"))) & (Bool (Set (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set (Var "G")) ")" )  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "I")))  ")" )  ")" ))))) ; 
 
theorem :: PDIFF_9:76 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )) "iff" (Bool (Set (Var "f"))  ($#r3_pdiff_9 :::"is_partial_differentiable_on"::: )  (Set (Var "Z")) "," (Set (Var "i")))  ")" ))))) ; 
 
theorem :: PDIFF_9:77 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "f"))  ($#k3_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set (Var "i")) ")" )))))) ; 
 
theorem :: PDIFF_9:78 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "j"))) "," (Set (Var "Z"))) & (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_pdiff_9 :::"`partial|"::: )   "(" (Set (Var "Z")) "," (Set (Var "I")) ")" )  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "Z")))))))) ; 
 
theorem :: PDIFF_9:79 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "Z"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "j")) "," (Set (Var "Z"))))))) ; 
 
theorem :: PDIFF_9:80 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "g")))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X")))  ")" ))))) ; 
 
theorem :: PDIFF_9:81 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  ) & (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X")))))))) ; 
 
theorem :: PDIFF_9:82 (Bool  "for" (Set (Var "m")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_pdiff_7 :::"open"::: )  )) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k1_euclid :::"REAL"::: )  (Set (Var "m")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X"))) & (Bool (Set (Var "g"))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")))  ($#r5_pdiff_9 :::"is_partial_differentiable_up_to_order"::: )  (Set (Var "i")) "," (Set (Var "X"))))))) ;