:: NDIFF_3  semantic presentation begin  














































theorem :: NDIFF_3:1 (Bool  "for" (Set (Var "G")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "G"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" ) & (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "G"))))  ")" )))) ; 
 
theorem :: NDIFF_3:2 (Bool  "for" (Set (Var "G")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "(" (Set (Var "s1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k1_ndiff_1 :::"(#)"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))))))) ; 
 definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "IT" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); attr "IT" is  :::"RestFunc-like":::  means :: NDIFF_3:def 1 (Bool  "("  (Bool "IT" "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool  "("   "for" (Set (Var "h")) "being"   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_fdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" "IT"  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" )) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" "IT"  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "F"))  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"RestFunc-like"::: NDIFF_3:def 1 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_ndiff_3 :::"RestFunc-like"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool  "("   "for" (Set (Var "h")) "being"   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_fdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" (Set (Var "IT"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" )) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" (Set (Var "IT"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "h")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" )  ")" )  ")" )  ")" ))); 
 registrationlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k1_numbers :::"REAL"::: )  )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_ndiff_3 :::"RestFunc-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))))); 
end; definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); mode RestFunc of "F" is   ($#v1_ndiff_3 :::"RestFunc-like"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"); end; definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "IT" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); attr "IT" is  :::"linear":::  means :: NDIFF_3:def 2 (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" "F" "st"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set "IT"  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "r")))))); end; 





:: deftheorem    defines :::"linear"::: NDIFF_3:def 2 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_ndiff_3 :::"linear"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "IT"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "r"))))))  ")" ))); 
 registrationlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster bbbadV1_XBOOLE_0() bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k1_numbers :::"REAL"::: )  )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v2_ndiff_3 :::"linear"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))))); 
end; definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); mode LinearFunc of "F" is   ($#v2_ndiff_3 :::"linear"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"); end; 










theorem :: NDIFF_3:3 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set (Var "L1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "L2"))) "is"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F"))) & (Bool (Set (Set (Var "L1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "L2"))) "is"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F")))  ")" ))) ; 
 
theorem :: NDIFF_3:4 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "L"))) "is"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F")))))) ; 
 
theorem :: NDIFF_3:5 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "h1")) "," (Set (Var "h2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "seq")))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "h1")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "h2")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "h2")) ")" )  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "h1"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" )  ($#k2_normsp_1 :::"+"::: )  (Set  "(" (Set (Var "h2"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "h1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "h2")) ")" )  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "h1"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "h2"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" )))  ")" )))) ; 
 
theorem :: NDIFF_3:6 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "h1")) "," (Set (Var "h2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "h1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "h2")) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "h2")) ")" )  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "h1"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" )  ($#k2_normsp_1 :::"+"::: )  (Set  "(" (Set (Var "h2"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "h1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "h2")) ")" )  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "h1"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "h2"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "seq")) ")" )))  ")" )))) ; 
 
theorem :: NDIFF_3:7 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set (Var "R1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "R2"))) "is"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F"))) & (Bool (Set (Set (Var "R1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "R2"))) "is"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")))  ")" ))) ; 
 
theorem :: NDIFF_3:8 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "R"))) "is"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")))))) ; 
 definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); let "x0" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; pred "f" :::"is_differentiable_in"::: "x0" means :: NDIFF_3:def 3 (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" "x0" "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "of" "F"(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" "F" "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "x0" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  "x0" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  "x0" ")" ) ")" ))))))  ")" )); end; 






:: deftheorem    defines :::"is_differentiable_in"::: NDIFF_3:def 3 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "x0")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) "iff" (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F"))(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")) "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  (Set (Var "x0")) ")" ) ")" ))))))  ")" ))  ")" )))); 
 definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); let "x0" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Set (Const "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Const "x0")))
 ; func  :::"diff":::  "(" "f" "," "x0" ")"  ->   ($#m1_subset_1 :::"Point":::) "of" "F" means :: NDIFF_3:def 4 (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" "x0" "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "of" "F"(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" "F" "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "x0" ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  "x0" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  "x0" ")" ) ")" )))  ")" )  ")" )))  ")" )); end; 








:: deftheorem    defines :::"diff"::: NDIFF_3:def 4 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "x0")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )) "iff" (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "F"))(Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")) "st"  (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x0")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  (Set (Var "x0")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "R"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "x"))  ($#k10_binop_2 :::"-"::: )  (Set (Var "x0")) ")" ) ")" )))  ")" )  ")" )))  ")" ))  ")" ))))); 
 definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); let "X" be    ($#m1_hidden :::"set"::: )  ; pred "f" :::"is_differentiable_on"::: "X" means :: NDIFF_3:def 5 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set "f"  ($#k2_partfun1 :::"|"::: )  "X")  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x")))  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_differentiable_on"::: NDIFF_3:def 5 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"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"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X")))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x")))  ")" )  ")" )  ")" )))); 
 
theorem :: NDIFF_3:9 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ))))) ; 
 
theorem :: NDIFF_3:10 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) "iff" (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: NDIFF_3:11 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y")) "is"   ($#v3_rcomp_1 :::"open"::: )  )))) ; 
 definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); let "X" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Const "X")))
 ; func "f" :::"`|"::: "X" ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F") means :: NDIFF_3:def 6 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" "f" "," (Set (Var "x")) ")" ))  ")" )  ")" ); end; 








:: deftheorem    defines :::"`|"::: NDIFF_3:def 6 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))  ")" )  ")" )  ")" ))))); 
 
theorem :: NDIFF_3:12 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" )  ")" )))) ; 
 
theorem :: NDIFF_3:13 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "x0")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k6_numbers :::"0"::: )  )  ($#v1_fdiff_1 :::"-convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v3_funct_1 :::"constant"::: )    ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "h"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "N")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set  "(" (Set (Var "h"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "c")) ")" ) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "c")) ")" ) ")" )) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set  "(" (Set (Var "h"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "c")) ")" ) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k8_funct_2 :::"/*"::: )  (Set (Var "c")) ")" ) ")" ) ")" )))  ")" ))))))) ; 
 
theorem :: NDIFF_3:14 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "f2"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "f2")))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x0")) ")"  ")" )))  ")" )))) ; 
 
theorem :: NDIFF_3:15 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set (Var "f2"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "f2")))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x0")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x0")) ")"  ")" )))  ")" )))) ; 
 
theorem :: NDIFF_3:16 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "f")))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0"))) & (Bool (Set   ($#k1_ndiff_3 :::"diff"::: )   "(" (Set  "(" (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x0")) ")"  ")" )))  ")" ))))) ; 
 
theorem :: NDIFF_3:17 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "f2"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "f2")))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k6_vfunct_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")"  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: NDIFF_3:18 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool (Set (Var "f2"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "f2")))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k2_vfunct_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f1")) "," (Set (Var "x")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f2")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" )))) ; 
 
theorem :: NDIFF_3:19 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "f")))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k1_ndiff_3 :::"diff"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )))  ")" )  ")" ))))) ; 
 
theorem :: NDIFF_3:20 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" )  ")" )))) ; 
 
theorem :: NDIFF_3:21 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "r")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_ndiff_3 :::"`|"::: )  (Set (Var "Z")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "r")))  ")" )  ")" ))))) ; 
 
theorem :: NDIFF_3:22 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_ndiff_3 :::"is_differentiable_in"::: )  (Set (Var "x0")))) "holds"  (Bool (Set (Var "f"))  ($#r1_nfcont_3 :::"is_continuous_in"::: )  (Set (Var "x0")))))) ; 
 
theorem :: NDIFF_3:23 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_nfcont_3 :::"continuous"::: )  )))) ; 
 
theorem :: NDIFF_3:24 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: NDIFF_3:25 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::) (Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "F")) "st"  (Bool  "("  (Bool (Set (Set (Var "R"))  ($#k7_partfun1 :::"/."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set (Var "R"))  ($#r1_nfcont_3 :::"is_continuous_in"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 definitionlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))); attr "f" is  :::"differentiable":::  means :: NDIFF_3:def 7 (Bool "f"  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")); end; 





:: deftheorem    defines :::"differentiable"::: NDIFF_3:def 7 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_ndiff_3 :::"differentiable"::: )  ) "iff" (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))  ")" ))); 
 registrationlet "F" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster bbbadV1_XBOOLE_0() bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k1_numbers :::"REAL"::: )  )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v3_ndiff_3 :::"differentiable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))))); 
end; 
theorem :: NDIFF_3:26 (Bool  "for" (Set (Var "F")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#v3_ndiff_3 :::"differentiable"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "f"))  ($#r2_ndiff_3 :::"is_differentiable_on"::: )  (Set (Var "Z")))))) ;