:: NDIFF_5 semantic presentation begin theorem :: NDIFF_5:1 (Bool "for" (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_ndiff_3 :::"RestFunc-like"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#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 "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k8_binop_2 :::"""::: ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "R")) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))) ")" ))) ; theorem :: NDIFF_5:2 (Bool "for" (Set (Var "S")) "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")) "st" (Bool (Bool (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) "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 :::"Real":::) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "h")) ($#k17_complex1 :::".|"::: ) ) ($#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")) ($#k11_binop_2 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "h")) ($#k17_complex1 :::".|"::: ) ))) ")" ) ")" ))))) ; theorem :: NDIFF_5: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 "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) (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 "L")) ($#k1_partfun1 :::"*"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "T")))))) ; theorem :: NDIFF_5: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 "R1")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k7_partfun1 :::"/."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "R2")) ($#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 "L")) "being" ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "S")) "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 "T"))))))) ; theorem :: NDIFF_5: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 "R1")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k7_partfun1 :::"/."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "R2")) ($#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 "L1")) "being" ($#m1_subset_1 :::"LinearFunc":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "L2")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "S")) "," (Set (Var "T")) "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 "T")))))))) ; theorem :: NDIFF_5:6 (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 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "st" (Bool (Bool (Set (Var "g")) ($#r1_ndiff_3 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r1_ndiff_3 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_ndiff_3 :::"diff"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" ) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set "(" ($#k1_ndiff_3 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "x0")) ")" ")" ))) ")" ))))) ; theorem :: NDIFF_5:7 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "xseq")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "yseq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "xseq"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "yseq")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "xseq"))))) "holds" (Bool (Set (Set (Var "yseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "xseq")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_normsp_0 :::".||"::: ) )) ")" )) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "xseq")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "yseq"))))))) ; theorem :: NDIFF_5:8 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x")) "holds" (Bool (Set (Set (Var "N1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N2"))) "is" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x")))))) ; theorem :: NDIFF_5:9 (Bool "for" (Set (Var "X")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"FinSequence":::)))) ; registrationlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); cluster (Set ($#k14_prvect_2 :::"product"::: ) "G") -> ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); let "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Const "G")) ")" )); let "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G"))); :: original: :::"."::: redefine func "z" :::"."::: "j" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" "G" ($#k3_prvect_2 :::"."::: ) "j" ")" ); end; theorem :: NDIFF_5:10 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )))) ; theorem :: NDIFF_5:11 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ))))))) ; definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); attr "G" is :::"non-trivial"::: means :: NDIFF_5:def 1 (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "G") "holds" (Bool (Bool "not" (Set "G" ($#k11_prvect_2 :::"."::: ) (Set (Var "j"))) "is" ($#v7_struct_0 :::"trivial"::: ) ))); end; :: deftheorem defines :::"non-trivial"::: NDIFF_5:def 1 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_ndiff_5 :::"non-trivial"::: ) ) "iff" (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Bool "not" (Set (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "j"))) "is" ($#v7_struct_0 :::"trivial"::: ) ))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ($#v1_ndiff_5 :::"non-trivial"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G"))); cluster (Set "G" ($#k1_funct_1 :::"."::: ) "i") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) for ($#l1_normsp_1 :::"RealNormSpace":::); end; registrationlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); cluster (Set ($#k14_prvect_2 :::"product"::: ) "G") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; theorem :: NDIFF_5:12 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "r0")) "," (Set (Var "p0")) "," (Set (Var "q0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p0"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q0")))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "r0"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "r0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "q0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))) ; theorem :: NDIFF_5:13 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "r0")) "," (Set (Var "p0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r0"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "r0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "p0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))))) ; theorem :: NDIFF_5:14 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "p0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p0"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "p0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))) ; theorem :: NDIFF_5:15 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "r0")) "," (Set (Var "p0")) "," (Set (Var "q0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p0"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q0")))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "r0"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "r0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "q0")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))) ; begin definitionlet "S" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); func :::"].":::"p" "," "q":::".["::: -> ($#m1_subset_1 :::"Subset":::) "of" "S" equals :: NDIFF_5:def 2 "{" (Set "(" "p" ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "q" ($#k5_algstr_0 :::"-"::: ) "p" ")" ) ")" ) ")" ) where t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) "}" ; end; :: deftheorem defines :::"]."::: NDIFF_5:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) where t "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) "}" ))); notationlet "S" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); synonym :::"[.":::"p" "," "q":::".]"::: for :::"LSeg"::: "(" "p" "," "q" ")" ; end; theorem :: NDIFF_5:16 (Bool "for" (Set (Var "S")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) )))) ; theorem :: NDIFF_5:17 (Bool "for" (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 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_ndiff_3 :::"RestFunc-like"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#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 "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))) ")" ))) ; theorem :: NDIFF_5:18 (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_fdiff_1 :::"RestFunc-like"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#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 "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set (Var "z")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))) ")" )) ; theorem :: NDIFF_5:19 (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 "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_nfcont_1 :::"is_continuous_in"::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "M"))) ")" )) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "q")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "p")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k11_binop_2 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))))))) ; theorem :: NDIFF_5:20 (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 "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) "st" (Bool (Bool (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_nfcont_1 :::"is_continuous_in"::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "L")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "M"))) ")" )) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "q")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "p")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k11_binop_2 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))))))) ; begin definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G"))); func :::"proj"::: "i" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) "G" ")" ) "," (Set "(" "G" ($#k11_prvect_2 :::"."::: ) "i" ")" ) means :: NDIFF_5:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_ndiff_5 :::"."::: ) "i"))); end; :: deftheorem defines :::"proj"::: NDIFF_5:def 3 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "i"))))) ")" )))); definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G"))); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ); func :::"reproj"::: "(" "i" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "G" ($#k11_prvect_2 :::"."::: ) "i" ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) "G" ")" ) means :: NDIFF_5:def 4 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" "G" ($#k11_prvect_2 :::"."::: ) "i" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "r")) ")" ))); end; :: deftheorem defines :::"reproj"::: NDIFF_5:def 4 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "r")) ")" ))) ")" ))))); definitionlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); let "j" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G")))) ; func :::"modetrans"::: "(" "G" "," "j" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "G") equals :: NDIFF_5:def 5 "j"; end; :: deftheorem defines :::"modetrans"::: NDIFF_5:def 5 : (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "j"))))); definitionlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); let "F" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "i" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ) "," (Set (Const "F")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ); pred "f" :::"is_partial_differentiable_in"::: "x" "," "i" means :: NDIFF_5:def 6 (Bool (Set "f" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" "G" "," "i" ")" ")" ) "," "x" ")" ")" )) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" "G" "," "i" ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) "x")); end; :: deftheorem defines :::"is_partial_differentiable_in"::: NDIFF_5:def 6 : (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" )) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" )))))); definitionlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); let "F" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "i" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ) "," (Set (Const "F")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ); func :::"partdiff"::: "(" "f" "," "x" "," "i" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" "G" ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" "G" "," "i" ")" ")" ) ")" ) "," "F" ")" ")" ) equals :: NDIFF_5:def 7 (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" "f" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" "G" "," "i" ")" ")" ) "," "x" ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" "G" "," "i" ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) "x" ")" ) ")" ); end; :: deftheorem defines :::"partdiff"::: NDIFF_5:def 7 : (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "holds" (Bool (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))))); begin definitionlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); let "F" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "i" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ) "," (Set (Const "F")); let "X" be ($#m1_hidden :::"set"::: ) ; pred "f" :::"is_partial_differentiable_on"::: "X" "," "i" means :: NDIFF_5:def 8 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) "G" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "X") ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," "i") ")" ) ")" ); end; :: deftheorem defines :::"is_partial_differentiable_on"::: NDIFF_5:def 8 : (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"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" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "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_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) ")" ) ")" ) ")" )))))); theorem :: NDIFF_5:21 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "xi")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "xi")) ($#k1_normsp_0 :::".||"::: ) ))))) ; theorem :: NDIFF_5:22 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) & (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "r")) ")" ))) ")" ))))) ; theorem :: NDIFF_5:23 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "st" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))))))))) ; theorem :: NDIFF_5:24 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "T")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"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" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) ")" ) ")" ) ")" )))))) ; theorem :: NDIFF_5:25 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "X")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" )))))) ; definitionlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); let "S" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "i" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G")))) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Const "G")) ")" ) "," (Set (Const "S")); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r2_ndiff_5 :::"is_partial_differentiable_on"::: ) (Set (Const "X")) "," (Set (Const "i"))) ; func "f" :::"`partial|"::: "(" "X" "," "i" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) "G" ")" ) "," (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" "G" ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" "G" "," "i" ")" ")" ) ")" ) "," "S" ")" ")" ) means :: NDIFF_5:def 9 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) "G" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" "f" "," (Set (Var "x")) "," "i" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`partial|"::: NDIFF_5:def 9 : (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) "," (Set (Var "S")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_ndiff_5 :::"`partial|"::: ) "(" (Set (Var "X")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b6")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))))))); theorem :: NDIFF_5:26 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" ))) ")" )))))) ; theorem :: NDIFF_5:27 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ))))))))) ; theorem :: NDIFF_5:28 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "f1")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set (Var "f2")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ))) ")" )))))) ; theorem :: NDIFF_5:29 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "f1")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set (Var "f2")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ))) ")" )))))) ; theorem :: NDIFF_5:30 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ))) ")" ))))))) ; begin theorem :: NDIFF_5:31 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))))) ; registrationlet "G" be ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::); cluster -> (Set ($#k3_finseq_1 :::"len"::: ) "G") ($#v3_card_1 :::"-element"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) "G" ")" )); end; theorem :: NDIFF_5:32 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"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" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) ")" ) ")" ) ")" )))))) ; theorem :: NDIFF_5:33 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set (Var "z")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "implies" (Bool (Set (Set (Var "z")) ($#k1_ndiff_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ")" ))))) ; theorem :: NDIFF_5:34 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))))) ; theorem :: NDIFF_5:35 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "holds" (Bool (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))))) ; theorem :: NDIFF_5:36 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))))) ; theorem :: NDIFF_5:37 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "holds" (Bool (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))))) ; theorem :: NDIFF_5:38 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" )))))) ; theorem :: NDIFF_5:39 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: NDIFF_5:40 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: NDIFF_5:41 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ))) ")" )))))) ; theorem :: NDIFF_5:42 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g")))))) ; theorem :: NDIFF_5:43 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "y")) ($#k11_card_3 :::"|"::: ) (Set (Var "Z")) ")" )) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )))))) ; theorem :: NDIFF_5:44 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "Z")) "," (Set (Var "x0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Z")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x0")) ($#k11_card_3 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))))) ; theorem :: NDIFF_5:45 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" )(Bool "ex" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "Z")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool "(" (Bool (Set (Var "y0")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Z")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "y0")) ($#k11_card_3 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "hi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "hi")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "hi")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))) ")" ) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g")))) ")" )))))))) ; theorem :: NDIFF_5:46 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "xi"))))) "holds" (Bool (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "xi"))))))) ; theorem :: NDIFF_5:47 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))))))) ; theorem :: NDIFF_5:48 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "xi"))))) "holds" (Bool (Set ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" )))))) ; theorem :: NDIFF_5:49 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "xi")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "j")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "j")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))))))) ; theorem :: NDIFF_5:50 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "F")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set (Var "F")) "st" (Bool (Bool (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "xi"))) & (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )))) "holds" (Bool (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "xi")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ))))))))) ; theorem :: NDIFF_5:51 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) "," (Set (Var "F")) ")" ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ndiff_5 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_ndiff_5 :::".["::: ) ))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "h")) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "L")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "M"))) ")" ) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) "," (Set (Var "i"))) ")" )) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k11_binop_2 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))))))))))) ; theorem :: NDIFF_5:52 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_rltopsp1 :::".]"::: ) )) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r"))))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))))))) ; theorem :: NDIFF_5:53 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) (Bool "for" (Set (Var "d")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_5 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) "," (Set (Var "i")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "y")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#k11_binop_2 :::"*"::: ) (Set (Var "r")))))))))))) ; theorem :: NDIFF_5:54 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y0")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y0"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Z")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "y0")) ($#k11_card_3 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ndiff_5 :::"reproj"::: ) "(" (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ")" ")" ) "," (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ")" )))))))) ; theorem :: NDIFF_5:55 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y0")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y0"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Z")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "y0")) ($#k11_card_3 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))))))) ; theorem :: NDIFF_5:56 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f")) ($#k7_ndiff_5 :::"`partial|"::: ) "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) ($#r3_nfcont_1 :::"is_continuous_on"::: ) (Set (Var "X"))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_ndiff_5 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set "(" ($#k3_ndiff_5 :::"proj"::: ) (Set "(" ($#k5_ndiff_5 :::"modetrans"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "h")) ")" ))) ")" ) & (Bool (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "w")))) ")" )) ")" ) ")" )))))) ; theorem :: NDIFF_5:57 (Bool "for" (Set (Var "G")) "being" ($#v1_ndiff_5 :::"non-trivial"::: ) ($#m1_hidden :::"RealNormSpace-Sequence":::) (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 "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "," (Set (Var "F")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_5 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f")) ($#k7_ndiff_5 :::"`partial|"::: ) "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) ($#r3_nfcont_1 :::"is_continuous_on"::: ) (Set (Var "X"))) ")" ) ")" ) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "X"))) ($#r3_nfcont_1 :::"is_continuous_on"::: ) (Set (Var "X"))) ")" ) ")" ))))) ;