:: PDIFF_3 semantic presentation begin registration cluster bbbadV1_FUNCT_1() ($#v2_fdiff_1 :::"RestFunc-like"::: ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "n" 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 "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"pdiff1"::: "(" "f" "," "i" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_3:def 1 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," (Set (Var "z")) "," "i" ")" ))); end; :: deftheorem defines :::"pdiff1"::: PDIFF_3:def 1 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (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 "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) "," (Set (Var "i")) ")" ))) ")" ))))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)); pred "f" :::"is_hpartial_differentiable`11_in"::: "z" means :: PDIFF_3:def 2 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" )))))) ")" )) ")" )); pred "f" :::"is_hpartial_differentiable`12_in"::: "z" means :: PDIFF_3:def 3 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" )))))) ")" )) ")" )); pred "f" :::"is_hpartial_differentiable`21_in"::: "z" means :: PDIFF_3:def 4 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" )))))) ")" )) ")" )); pred "f" :::"is_hpartial_differentiable`22_in"::: "z" means :: PDIFF_3:def 5 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" )))))) ")" )) ")" )); end; :: deftheorem defines :::"is_hpartial_differentiable`11_in"::: PDIFF_3:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z"))) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" )))))) ")" )) ")" )) ")" ))); :: deftheorem defines :::"is_hpartial_differentiable`12_in"::: PDIFF_3:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z"))) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" )))))) ")" )) ")" )) ")" ))); :: deftheorem defines :::"is_hpartial_differentiable`21_in"::: PDIFF_3:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z"))) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" )))))) ")" )) ")" )) ")" ))); :: deftheorem defines :::"is_hpartial_differentiable`22_in"::: PDIFF_3:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z"))) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" )))))) ")" )) ")" )) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)); assume (Bool (Set (Const "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Const "z"))) ; func :::"hpartdiff11"::: "(" "f" "," "z" ")" -> ($#m1_subset_1 :::"Real":::) means :: PDIFF_3:def 6 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"hpartdiff11"::: PDIFF_3:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)); assume (Bool (Set (Const "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Const "z"))) ; func :::"hpartdiff12"::: "(" "f" "," "z" ")" -> ($#m1_subset_1 :::"Real":::) means :: PDIFF_3:def 7 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 1) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"hpartdiff12"::: PDIFF_3:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)); assume (Bool (Set (Const "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Const "z"))) ; func :::"hpartdiff21"::: "(" "f" "," "z" ")" -> ($#m1_subset_1 :::"Real":::) means :: PDIFF_3:def 8 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"hpartdiff21"::: PDIFF_3:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)); assume (Bool (Set (Const "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Const "z"))) ; func :::"hpartdiff22"::: "(" "f" "," "z" ")" -> ($#m1_subset_1 :::"Real":::) means :: PDIFF_3:def 9 (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" "f" "," (Num 2) ")" ")" ) "," "z" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"hpartdiff22"::: PDIFF_3:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "y0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::)(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y")) ($#k9_real_1 :::"-"::: ) (Set (Var "y0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )) ")" )))); theorem :: PDIFF_3:1 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))))) ; theorem :: PDIFF_3:2 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0")))))) ; theorem :: PDIFF_3:3 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))))) ; theorem :: PDIFF_3:4 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0")))))) ; theorem :: PDIFF_3:5 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) "," (Set (Var "x0")) ")" ))))) ; theorem :: PDIFF_3:6 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) ")" ")" ) "," (Set (Var "y0")) ")" ))))) ; theorem :: PDIFF_3:7 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) "," (Set (Var "x0")) ")" ))))) ; theorem :: PDIFF_3:8 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) ")" ")" ) "," (Set (Var "y0")) ")" ))))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_hidden :::"set"::: ) ; pred "f" :::"is_hpartial_differentiable`11_on"::: "Z" means :: PDIFF_3:def 10 (Bool "(" (Bool "Z" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "Z") ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z"))) ")" ) ")" ); pred "f" :::"is_hpartial_differentiable`12_on"::: "Z" means :: PDIFF_3:def 11 (Bool "(" (Bool "Z" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "Z") ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z"))) ")" ) ")" ); pred "f" :::"is_hpartial_differentiable`21_on"::: "Z" means :: PDIFF_3:def 12 (Bool "(" (Bool "Z" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "Z") ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z"))) ")" ) ")" ); pred "f" :::"is_hpartial_differentiable`22_on"::: "Z" means :: PDIFF_3:def 13 (Bool "(" (Bool "Z" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "Z") ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z"))) ")" ) ")" ); end; :: deftheorem defines :::"is_hpartial_differentiable`11_on"::: PDIFF_3:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r5_pdiff_3 :::"is_hpartial_differentiable`11_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 "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z"))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_hpartial_differentiable`12_on"::: PDIFF_3:def 11 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r6_pdiff_3 :::"is_hpartial_differentiable`12_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 "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z"))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_hpartial_differentiable`21_on"::: PDIFF_3:def 12 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r7_pdiff_3 :::"is_hpartial_differentiable`21_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 "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z"))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_hpartial_differentiable`22_on"::: PDIFF_3:def 13 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r8_pdiff_3 :::"is_hpartial_differentiable`22_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 "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z"))) ")" ) ")" ) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r5_pdiff_3 :::"is_hpartial_differentiable`11_on"::: ) (Set (Const "Z"))) ; func "f" :::"`hpartial11|"::: "Z" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_3:def 14 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "Z") & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" "f" "," (Set (Var "z")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`hpartial11|"::: PDIFF_3:def 14 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r5_pdiff_3 :::"is_hpartial_differentiable`11_on"::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_pdiff_3 :::"`hpartial11|"::: ) (Set (Var "Z")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r6_pdiff_3 :::"is_hpartial_differentiable`12_on"::: ) (Set (Const "Z"))) ; func "f" :::"`hpartial12|"::: "Z" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_3:def 15 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "Z") & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" "f" "," (Set (Var "z")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`hpartial12|"::: PDIFF_3:def 15 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r6_pdiff_3 :::"is_hpartial_differentiable`12_on"::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_pdiff_3 :::"`hpartial12|"::: ) (Set (Var "Z")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r7_pdiff_3 :::"is_hpartial_differentiable`21_on"::: ) (Set (Const "Z"))) ; func "f" :::"`hpartial21|"::: "Z" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_3:def 16 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "Z") & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" "f" "," (Set (Var "z")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`hpartial21|"::: PDIFF_3:def 16 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r7_pdiff_3 :::"is_hpartial_differentiable`21_on"::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_pdiff_3 :::"`hpartial21|"::: ) (Set (Var "Z")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r8_pdiff_3 :::"is_hpartial_differentiable`22_on"::: ) (Set (Const "Z"))) ; func "f" :::"`hpartial22|"::: "Z" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_3:def 17 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "Z") & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "Z")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" "f" "," (Set (Var "z")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`hpartial22|"::: PDIFF_3:def 17 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r8_pdiff_3 :::"is_hpartial_differentiable`22_on"::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k9_pdiff_3 :::"`hpartial22|"::: ) (Set (Var "Z")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" )) ")" ) ")" ) ")" )))); begin theorem :: PDIFF_3:9 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z"))) "iff" (Bool (Set ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z")) "," (Num 1)) ")" ))) ; theorem :: PDIFF_3:10 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z"))) "iff" (Bool (Set ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z")) "," (Num 2)) ")" ))) ; theorem :: PDIFF_3:11 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z"))) "iff" (Bool (Set ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z")) "," (Num 1)) ")" ))) ; theorem :: PDIFF_3:12 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z"))) "iff" (Bool (Set ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z")) "," (Num 2)) ")" ))) ; theorem :: PDIFF_3:13 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) "," (Num 1) ")" )))) ; theorem :: PDIFF_3:14 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z")) "," (Num 2) ")" )))) ; theorem :: PDIFF_3:15 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) "," (Num 1) ")" )))) ; theorem :: PDIFF_3:16 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z")) "," (Num 2) ")" )))) ; theorem :: PDIFF_3:17 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" )))) "holds" (Bool "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_3:18 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0"))) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" )))) "holds" (Bool "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_3:19 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0"))) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" )))) "holds" (Bool "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_3:20 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0"))) "st" (Bool (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" )))) "holds" (Bool "for" (Set (Var "h")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_3:21 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:22 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:23 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:24 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:25 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:26 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:27 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:28 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f1")) "," (Set (Var "z0")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f2")) "," (Set (Var "z0")) ")" ")" ))) ")" ))) ; theorem :: PDIFF_3:29 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_pdiff_3 :::"hpartdiff11"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" ))) ")" )))) ; theorem :: PDIFF_3:30 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_pdiff_3 :::"hpartdiff12"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" ))) ")" )))) ; theorem :: PDIFF_3:31 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_pdiff_3 :::"hpartdiff21"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" ))) ")" )))) ; theorem :: PDIFF_3:32 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) ")" ) "," (Set (Var "z0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_pdiff_3 :::"hpartdiff22"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" ))) ")" )))) ; theorem :: PDIFF_3:33 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)))) ; theorem :: PDIFF_3:34 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 1) ")" ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 1) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)))) ; theorem :: PDIFF_3:35 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 1)))) ; theorem :: PDIFF_3:36 (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "f2")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f1")) "," (Num 2) ")" ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f2")) "," (Num 2) ")" ")" )) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z0")) "," (Num 2)))) ; theorem :: PDIFF_3:37 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_3 :::"is_hpartial_differentiable`11_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")))))) ; theorem :: PDIFF_3:38 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_3 :::"is_hpartial_differentiable`12_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) "," (Set (Var "z0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")))))) ; theorem :: PDIFF_3:39 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_3 :::"is_hpartial_differentiable`21_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")))))) ; theorem :: PDIFF_3:40 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "f")) ($#r4_pdiff_3 :::"is_hpartial_differentiable`22_in"::: ) (Set (Var "z0")))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set "(" ($#k1_pdiff_3 :::"pdiff1"::: ) "(" (Set (Var "f")) "," (Num 2) ")" ")" ) "," (Set (Var "z0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")))))) ;