:: NDIFF_2 semantic presentation begin definitionlet "X", "Y", "Z" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Const "X")) "," (Set (Const "Y")) ")" ); let "g" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Const "Y")) "," (Set (Const "Z")) ")" ); func "g" :::"*"::: "f" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "Z" ")" ) equals :: NDIFF_2:def 1 (Set (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" "g" "," "Y" "," "Z" ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" "f" "," "X" "," "Y" ")" ")" )); end; :: deftheorem defines :::"*"::: NDIFF_2:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k1_ndiff_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" (Set (Var "g")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )))))); definitionlet "X", "Y", "Z" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Const "X")) "," (Set (Const "Y")) ")" ")" ); let "g" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Const "Y")) "," (Set (Const "Z")) ")" ")" ); func "g" :::"*"::: "f" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" "X" "," "Z" ")" ")" ) equals :: NDIFF_2:def 2 (Set (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" "g" "," "Y" "," "Z" ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" "f" "," "X" "," "Y" ")" ")" )); end; :: deftheorem defines :::"*"::: NDIFF_2:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "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 "X")) "," (Set (Var "Y")) ")" ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k2_ndiff_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" (Set (Var "g")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )))))); theorem :: NDIFF_2:1 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (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 :::"sequence":::) "of" (Set (Var "S")) "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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set (Var "z"))) ($#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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" ))) ")" ) ")" ))))) ; theorem :: NDIFF_2:2 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (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 :::"sequence":::) "of" (Set (Var "S")) "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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set (Var "z"))) ($#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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" ))))))) ; theorem :: NDIFF_2:3 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "dv")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (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 :::"sequence":::) "of" (Set (Var "S")) "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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Var "dv")) ($#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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )) ")" ) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x0"))) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "dv")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ) ")" ))) ")" ))))))) ; definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "x0", "z" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); pred "f" :::"is_Gateaux_differentiable_in"::: "x0" "," "z" means :: NDIFF_2:def 3 (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" "x0" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "ex" (Set (Var "dv")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) "z" ")" ) ($#k3_rlvect_1 :::"+"::: ) "x0") ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) "z" ")" ) ($#k3_rlvect_1 :::"+"::: ) "x0" ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) "x0" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "dv")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ) ")" )))) ")" )); end; :: deftheorem defines :::"is_Gateaux_differentiable_in"::: NDIFF_2:def 3 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_2 :::"is_Gateaux_differentiable_in"::: ) (Set (Var "x0")) "," (Set (Var "z"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_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 "dv")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x0"))) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "dv")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ) ")" )))) ")" )) ")" )))); theorem :: NDIFF_2:4 (Bool "(" (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "e")) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "e")) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "e")) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "e")) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" ) ")" ) ; definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "x0", "z" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); assume (Bool (Set (Const "f")) ($#r1_ndiff_2 :::"is_Gateaux_differentiable_in"::: ) (Set (Const "x0")) "," (Set (Const "z"))) ; func :::"Gateaux_diff"::: "(" "f" "," "x0" "," "z" ")" -> ($#m1_subset_1 :::"Point":::) "of" "T" means :: NDIFF_2:def 4 (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" "x0" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) "z" ")" ) ($#k3_rlvect_1 :::"+"::: ) "x0") ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) "z" ")" ) ($#k3_rlvect_1 :::"+"::: ) "x0" ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) "x0" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) it ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Gateaux_diff"::: NDIFF_2:def 4 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_2 :::"is_Gateaux_differentiable_in"::: ) (Set (Var "x0")) "," (Set (Var "z")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_2 :::"Gateaux_diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "z")) ")" )) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x0"))) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "h")) ($#k2_real_1 :::"""::: ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b6")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ) ")" )) ")" ) ")" )) ")" ))))); theorem :: NDIFF_2:5 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_2 :::"is_Gateaux_differentiable_in"::: ) (Set (Var "x0")) "," (Set (Var "z"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_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 "dv")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (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 :::"sequence":::) "of" (Set (Var "S")) "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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Var "dv")) ($#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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))) ")" )) ")" )))) ; theorem :: NDIFF_2:6 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_2 :::"is_Gateaux_differentiable_in"::: ) (Set (Var "x0")) "," (Set (Var "z"))) & (Bool (Set ($#k3_ndiff_2 :::"Gateaux_diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set (Var "z")))) & (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (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 :::"sequence":::) "of" (Set (Var "S")) "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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k3_ndiff_2 :::"Gateaux_diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "z")) ")" ) ($#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 "(" (Set (Var "h")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )) ")" ) ")" )) ")" ))))) ; theorem :: NDIFF_2:7 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "h")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "h")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "e")) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "h")) ($#k1_normsp_0 :::".||"::: ) ))) ")" ) ")" ))))) ; theorem :: NDIFF_2:8 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "," (Set (Var "U")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "T")) "," (Set (Var "U")) "st" (Bool (Bool (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "U"))))) "holds" (Bool "for" (Set (Var "L")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set (Set (Var "R")) ($#k1_partfun1 :::"*"::: ) (Set (Var "L"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "U")))))) ; theorem :: NDIFF_2:9 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "U")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "L")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "T")) "," (Set (Var "U")) "holds" (Bool (Set (Set (Var "L")) ($#k1_partfun1 :::"*"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "U")))))) ; theorem :: NDIFF_2:10 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "U")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R1")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "T")) "," (Set (Var "U")) "st" (Bool (Bool (Set (Set (Var "R2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "U"))))) "holds" (Bool (Set (Set (Var "R2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "R1"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "U")))))) ; theorem :: NDIFF_2:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "U")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R1")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "T")) "," (Set (Var "U")) "st" (Bool (Bool (Set (Set (Var "R2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "U"))))) "holds" (Bool "for" (Set (Var "L")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set (Set (Var "R2")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "R1")) ")" )) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "U"))))))) ; theorem :: NDIFF_2:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "U")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R1")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "T")) "," (Set (Var "U")) "st" (Bool (Bool (Set (Set (Var "R2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "U"))))) "holds" (Bool "for" (Set (Var "L1")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "L2")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "T")) "," (Set (Var "U")) "holds" (Bool (Set (Set "(" (Set (Var "L2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "R1")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "R2")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "L1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "R1")) ")" ) ")" )) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "U")))))))) ; theorem :: NDIFF_2:13 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "T")) "," (Set (Var "U")) "st" (Bool (Bool (Set (Var "f2")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" ) ")" ")" ) ($#k2_ndiff_2 :::"*"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x0")) ")" ")" ))) ")" )))))) ;