:: PDIFF_6 semantic presentation begin theorem :: PDIFF_6:1 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" )) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )) ")" ))) ; theorem :: PDIFF_6:2 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "g")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "y"))) ")" )))))) ; theorem :: PDIFF_6:3 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) ")" ))))))) ; theorem :: PDIFF_6:4 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_integr15 :::"+"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "g2"))))))) ; theorem :: PDIFF_6:5 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k8_integr15 :::"-"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "g2"))))))) ; theorem :: PDIFF_6:6 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "a")) ($#k9_integr15 :::"(#)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "g")))))))) ; theorem :: PDIFF_6:7 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) ")" ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_integr15 :::"+"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2"))))))) ; theorem :: PDIFF_6:8 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) ")" ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k8_integr15 :::"-"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2"))))))) ; theorem :: PDIFF_6:9 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) ")" ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "r")) ($#k9_integr15 :::"(#)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")))))))) ; theorem :: PDIFF_6:10 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) ")" ")" ))))) ; definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "IT" is :::"additive"::: means :: PDIFF_6:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "m") "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))); attr "IT" is :::"homogeneous"::: means :: PDIFF_6:def 2 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "m") (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); end; :: deftheorem defines :::"additive"::: PDIFF_6:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_pdiff_6 :::"additive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))) ")" ))); :: deftheorem defines :::"homogeneous"::: PDIFF_6:def 2 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_pdiff_6 :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" ))); theorem :: PDIFF_6:11 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "IT")) "is" ($#v1_pdiff_6 :::"additive"::: ) )) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: PDIFF_6:12 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_pdiff_6 :::"additive"::: ) ) "iff" (Bool (Set (Var "g")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) ")" )))) ; theorem :: PDIFF_6:13 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_pdiff_6 :::"homogeneous"::: ) ) "iff" (Bool (Set (Var "g")) "is" ($#v1_lopban_1 :::"homogeneous"::: ) ) ")" )))) ; registrationlet "n", "m" be ($#m1_hidden :::"Nat":::); cluster (Set (Set "(" ($#k1_euclid :::"REAL"::: ) "m" ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) "n" ")" )) -> ($#v1_pdiff_6 :::"additive"::: ) ($#v2_pdiff_6 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "m" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ); end; registrationlet "n", "m" be ($#m1_hidden :::"Nat":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k1_euclid :::"REAL"::: ) "m") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_euclid :::"REAL"::: ) "n") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k1_euclid :::"REAL"::: ) "m") "," (Set ($#k1_euclid :::"REAL"::: ) "n")) ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#v8_valued_2 :::"ext-real-functions-valued"::: ) ($#v9_valued_2 :::"real-functions-valued"::: ) ($#v1_pdiff_6 :::"additive"::: ) ($#v2_pdiff_6 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" ($#k1_euclid :::"REAL"::: ) "m" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ))))); end; definitionlet "m", "n" be ($#m1_hidden :::"Nat":::); mode LinearOperator of "m" "," "n" is ($#v1_pdiff_6 :::"additive"::: ) ($#v2_pdiff_6 :::"homogeneous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "m" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ); end; theorem :: PDIFF_6:14 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "m")) "," (Set (Var "n"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )) ")" ))) ; definitionlet "m", "n" be ($#m1_hidden :::"Nat":::); let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); :: original: :::"."::: redefine func "IT" :::"."::: "x" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; definitionlet "m", "n" be ($#m1_hidden :::"Nat":::); let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "IT" is :::"Lipschitzian"::: means :: PDIFF_6:def 3 (Bool "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "m") "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" "IT" ($#k1_pdiff_6 :::"."::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "K")) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))) ")" ) ")" )); end; :: deftheorem defines :::"Lipschitzian"::: PDIFF_6:def 3 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_pdiff_6 :::"Lipschitzian"::: ) ) "iff" (Bool "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "IT")) ($#k1_pdiff_6 :::"."::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "K")) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))) ")" ) ")" )) ")" ))); theorem :: PDIFF_6:15 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "xseq")) "," (Set (Var "yseq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "xseq"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "yseq")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set (Var "xseq")) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "yseq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "yseq")))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "xseq")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "xseq")) ")" ))) & (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "xseq"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "yseq")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "v")))) ")" )))) ; theorem :: PDIFF_6:16 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "m")) "," (Set (Var "n")) (Bool "for" (Set (Var "xseq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "yseq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "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" ($#m1_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_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "xseq")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "yseq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_pdiff_6 :::"."::: ) (Set "(" ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "xseq")) ")" ))))))) ; theorem :: PDIFF_6:17 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "xseq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (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" ($#m1_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 "ex" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "xseq")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "yseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "v")) ($#k12_euclid :::".|"::: ) )) ")" )) ")" )) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "xseq")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "yseq"))))))) ; registrationlet "m", "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k1_euclid :::"REAL"::: ) "m") "," (Set ($#k1_euclid :::"REAL"::: ) "n")) ($#v1_pdiff_6 :::"additive"::: ) ($#v2_pdiff_6 :::"homogeneous"::: ) -> ($#v3_pdiff_6 :::"Lipschitzian"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" ($#k1_euclid :::"REAL"::: ) "m" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ))))); end; registrationlet "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" ))) ($#v13_vectsp_1 :::"additive"::: ) ($#v1_lopban_1 :::"homogeneous"::: ) -> ($#v2_lopban_1 :::"Lipschitzian"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" )))))); end; theorem :: PDIFF_6:18 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ))))) ; theorem :: PDIFF_6:19 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "m")) "," (Set (Var "n")))))) ; theorem :: PDIFF_6:20 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "g1")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0"))) & (Bool (Set (Var "g2")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0")))) "holds" (Bool "(" (Bool (Set (Set (Var "g1")) ($#k7_integr15 :::"+"::: ) (Set (Var "g2"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0"))) & (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "g1")) ($#k7_integr15 :::"+"::: ) (Set (Var "g2")) ")" ) "," (Set (Var "y0")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "y0")) ")" ")" ) ($#k7_integr15 :::"+"::: ) (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "y0")) ")" ")" ))) ")" )))) ; theorem :: PDIFF_6:21 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "g1")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0"))) & (Bool (Set (Var "g2")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0")))) "holds" (Bool "(" (Bool (Set (Set (Var "g1")) ($#k8_integr15 :::"-"::: ) (Set (Var "g2"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0"))) & (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "g1")) ($#k8_integr15 :::"-"::: ) (Set (Var "g2")) ")" ) "," (Set (Var "y0")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "g1")) "," (Set (Var "y0")) ")" ")" ) ($#k8_integr15 :::"-"::: ) (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "g2")) "," (Set (Var "y0")) ")" ")" ))) ")" )))) ; theorem :: PDIFF_6:22 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k9_integr15 :::"(#)"::: ) (Set (Var "g"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0"))) & (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "r")) ($#k9_integr15 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set (Var "y0")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k9_integr15 :::"(#)"::: ) (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y0")) ")" ")" ))) ")" ))))) ; theorem :: PDIFF_6:23 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "y0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "y0")))) "holds" (Bool "{" (Set (Var "y")) where y "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y0")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ))))) ; theorem :: PDIFF_6:24 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "L")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "m")) "," (Set (Var "n"))) & (Bool "ex" (Set (Var "r0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r0"))) & (Bool "{" (Set (Var "y")) where y "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r0"))) "}" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (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" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "m")))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "z")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_pdiff_6 :::"."::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "z")) ($#k12_euclid :::".|"::: ) ) ($#k2_real_1 :::"""::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r0")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_pdiff_6 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_pdiff_6 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "L"))) ")" ))))) ; theorem :: PDIFF_6:25 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) "iff" (Bool "ex" (Set (Var "r0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r0"))) & (Bool "{" (Set (Var "y")) where y "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r0"))) "}" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "L")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "m")) "," (Set (Var "n"))) & (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" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "m")))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "z")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_pdiff_6 :::"."::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "z")) ($#k12_euclid :::".|"::: ) ) ($#k2_real_1 :::"""::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r0")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_pdiff_6 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_pdiff_6 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" )) ")" )) ")" )))) ; begin theorem :: PDIFF_6:26 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "y1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y2")) ")" ))))) ; theorem :: PDIFF_6:27 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y1")) ")" )))))) ; theorem :: PDIFF_6:28 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "g")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "x0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set (Var "x0")) ")" )) ")" ))))) ; theorem :: PDIFF_6:29 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "n", "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); pred "f" :::"is_differentiable_on"::: "X" means :: PDIFF_6:def 4 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "m") "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "X") ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ); end; :: deftheorem defines :::"is_differentiable_on"::: PDIFF_6:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_6 :::"is_differentiable_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ) ")" )))); theorem :: PDIFF_6:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_6 :::"is_differentiable_on"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "g")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) ")" ))))) ; theorem :: PDIFF_6:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_6 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ))))) ; theorem :: PDIFF_6:32 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool "ex" (Set (Var "Z0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Var "Z0"))) & (Bool (Set (Var "Z0")) "is" ($#v3_nfcont_1 :::"open"::: ) ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_6 :::"is_differentiable_on"::: ) (Set (Var "Z"))) "iff" (Bool "(" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ) ")" )))) ; theorem :: PDIFF_6:33 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_6 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "ex" (Set (Var "Z0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Var "Z0"))) & (Bool (Set (Var "Z0")) "is" ($#v3_nfcont_1 :::"open"::: ) ) ")" ))))) ;