:: PDIFF_4 semantic presentation begin theorem :: PDIFF_4:1 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Num 3))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ; theorem :: PDIFF_4:2 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Num 3))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ) ; theorem :: PDIFF_4:3 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 3) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Num 3))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 3) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 3) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ) ")" ) ; begin theorem :: PDIFF_4:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))))) ; theorem :: PDIFF_4:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y")))))) ; theorem :: PDIFF_4:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "z")))))) ; theorem :: PDIFF_4:7 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) ")" )) "iff" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1)) ")" ))) ; theorem :: PDIFF_4:8 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y0"))) ")" )) "iff" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2)) ")" ))) ; theorem :: PDIFF_4:9 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "z0"))) ")" )) "iff" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3)) ")" ))) ; theorem :: PDIFF_4:10 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1))) "holds" (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 (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#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")) ")" ) ")" )))))) ")" ))))) ; theorem :: PDIFF_4:11 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2))) "holds" (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 (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#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_4:12 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "z0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "z")) ($#k9_real_1 :::"-"::: ) (Set (Var "z0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "z")) ($#k9_real_1 :::"-"::: ) (Set (Var "z0")) ")" ) ")" )))))) ")" ))))) ; theorem :: PDIFF_4:13 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1)) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_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 (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#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")) ")" ) ")" )))))) ")" )) ")" )) ")" ))) ; theorem :: PDIFF_4:14 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2)) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_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 (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#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_4:15 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3)) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "z0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "z")) ($#k9_real_1 :::"-"::: ) (Set (Var "z0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "z")) ($#k9_real_1 :::"-"::: ) (Set (Var "z0")) ")" ) ")" )))))) ")" )) ")" )) ")" ))) ; theorem :: PDIFF_4:16 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 1) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_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 (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 "r")) ($#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 (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#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")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )) ")" )))) ; theorem :: PDIFF_4:17 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 2) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_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 (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 "r")) ($#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 (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#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_4:18 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 3) ")" )) "iff" (Bool "ex" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "z0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ))) & (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 "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "z")) ($#k9_real_1 :::"-"::: ) (Set (Var "z0")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "z")) ($#k9_real_1 :::"-"::: ) (Set (Var "z0")) ")" ) ")" ))) ")" ) ")" ))) ")" )) ")" )) ")" )))) ; theorem :: PDIFF_4:19 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) "," (Set (Var "x0")) ")" ))))) ; theorem :: PDIFF_4:20 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) "," (Set (Var "y0")) ")" ))))) ; theorem :: PDIFF_4:21 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 3) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u")) ")" ")" ) "," (Set (Var "z0")) ")" ))))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_hidden :::"set"::: ) ; pred "f" :::"is_partial_differentiable`1_on"::: "D" means :: PDIFF_4:def 1 (Bool "(" (Bool "D" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "D") ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1)) ")" ) ")" ); pred "f" :::"is_partial_differentiable`2_on"::: "D" means :: PDIFF_4:def 2 (Bool "(" (Bool "D" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "D") ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2)) ")" ) ")" ); pred "f" :::"is_partial_differentiable`3_on"::: "D" means :: PDIFF_4:def 3 (Bool "(" (Bool "D" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "D") ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3)) ")" ) ")" ); end; :: deftheorem defines :::"is_partial_differentiable`1_on"::: PDIFF_4:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_4 :::"is_partial_differentiable`1_on"::: ) (Set (Var "D"))) "iff" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1)) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_partial_differentiable`2_on"::: PDIFF_4:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_pdiff_4 :::"is_partial_differentiable`2_on"::: ) (Set (Var "D"))) "iff" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2)) ")" ) ")" ) ")" ))); :: deftheorem defines :::"is_partial_differentiable`3_on"::: PDIFF_4:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_4 :::"is_partial_differentiable`3_on"::: ) (Set (Var "D"))) "iff" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3)) ")" ) ")" ) ")" ))); theorem :: PDIFF_4:22 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_4 :::"is_partial_differentiable`1_on"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 1)) ")" ) ")" ))) ; theorem :: PDIFF_4:23 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_4 :::"is_partial_differentiable`2_on"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 2)) ")" ) ")" ))) ; theorem :: PDIFF_4:24 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_4 :::"is_partial_differentiable`3_on"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u")) "," (Num 3)) ")" ) ")" ))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r1_pdiff_4 :::"is_partial_differentiable`1_on"::: ) (Set (Const "D"))) ; func "f" :::"`partial1|"::: "D" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_4:def 4 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "D") & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," (Set (Var "u")) "," (Num 1) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`partial1|"::: PDIFF_4:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_4 :::"is_partial_differentiable`1_on"::: ) (Set (Var "D")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_pdiff_4 :::"`partial1|"::: ) (Set (Var "D")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 1) ")" )) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r2_pdiff_4 :::"is_partial_differentiable`2_on"::: ) (Set (Const "D"))) ; func "f" :::"`partial2|"::: "D" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_4:def 5 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "D") & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," (Set (Var "u")) "," (Num 2) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`partial2|"::: PDIFF_4:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_4 :::"is_partial_differentiable`2_on"::: ) (Set (Var "D")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_pdiff_4 :::"`partial2|"::: ) (Set (Var "D")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 2) ")" )) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r3_pdiff_4 :::"is_partial_differentiable`3_on"::: ) (Set (Const "D"))) ; func "f" :::"`partial3|"::: "D" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_4:def 6 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "D") & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," (Set (Var "u")) "," (Num 3) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`partial3|"::: PDIFF_4:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_4 :::"is_partial_differentiable`3_on"::: ) (Set (Var "D")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_pdiff_4 :::"`partial3|"::: ) (Set (Var "D")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u")) "," (Num 3) ")" )) ")" ) ")" ) ")" )))); begin theorem :: PDIFF_4:25 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0"))) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 1)) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" )))) "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 ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_rvsum_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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u0")) "," (Num 1) ")" ) ($#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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_4:26 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0"))) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 2)) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" )))) "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 ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_rvsum_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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u0")) "," (Num 2) ")" ) ($#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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#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 (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_4:27 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 3) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0"))) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 3)) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" )))) "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 ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 3) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0")) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_rvsum_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 3) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "u0")) "," (Num 3) ")" ) ($#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 3) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k3_valued_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ))) ")" )))))) ; theorem :: PDIFF_4:28 (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 1)) & (Bool (Set (Var "f2")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 1))) "holds" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 1)))) ; theorem :: PDIFF_4:29 (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 2)) & (Bool (Set (Var "f2")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 2))) "holds" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 2)))) ; theorem :: PDIFF_4:30 (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 3)) & (Bool (Set (Var "f2")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 3))) "holds" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 3)))) ; theorem :: PDIFF_4:31 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 1))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 1) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0")))))) ; theorem :: PDIFF_4:32 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 2))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 2) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 2) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0")))))) ; theorem :: PDIFF_4:33 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "u0")) "," (Num 3))) "holds" (Bool (Set ($#k1_pdiff_2 :::"SVF1"::: ) "(" (Num 3) "," (Set (Var "f")) "," (Set (Var "u0")) ")" ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 3) "," (Num 3) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "u0")))))) ; begin definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); func :::"grad"::: "(" "f" "," "p" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: PDIFF_4:def 7 (Set (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," "p" "," (Num 1) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," "p" "," (Num 2) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," "p" "," (Num 3) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )); end; :: deftheorem defines :::"grad"::: PDIFF_4:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))))); theorem :: PDIFF_4:34 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) "," (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) "," (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ; theorem :: PDIFF_4:35 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3))) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ")" ))))) ; theorem :: PDIFF_4:36 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3))) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set "(" (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k8_euclid :::"-"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ")" ))))) ; theorem :: PDIFF_4:37 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3))) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )))))) ; theorem :: PDIFF_4:38 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3))) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set "(" (Set "(" (Set (Var "s")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "t")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ")" ) ")" )))))) ; theorem :: PDIFF_4:39 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 1)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 2)) & (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "p")) "," (Num 3))) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set "(" (Set "(" (Set (Var "s")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k8_euclid :::"-"::: ) (Set "(" (Set (Var "t")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ")" ) ")" )))))) ; theorem :: PDIFF_4:40 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k16_euclid :::"0.REAL"::: ) (Num 3))))) ; definitionlet "a" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); func :::"unitvector"::: "a" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: PDIFF_4:def 8 (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ); end; :: deftheorem defines :::"unitvector"::: PDIFF_4:def 8 : (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k5_pdiff_4 :::"unitvector"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "p", "a" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); func :::"Directiondiff"::: "(" "f" "," "p" "," "a" ")" -> ($#m1_subset_1 :::"Real":::) equals :: PDIFF_4:def 9 (Set (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," "p" "," (Num 1) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) "a" ")" ) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," "p" "," (Num 2) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) "a" ")" ) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f" "," "p" "," (Num 3) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) "a" ")" ) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" )); end; :: deftheorem defines :::"Directiondiff"::: PDIFF_4:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k6_pdiff_4 :::"Directiondiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) (Set (Var "a")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) (Set (Var "a")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) (Set (Var "a")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 3) ")" ) ")" ))))); theorem :: PDIFF_4:41 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) "," (Set (Var "z0")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k6_pdiff_4 :::"Directiondiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x0")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y0")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "z0")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "y0")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x0")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y0")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "z0")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "z0")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x0")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y0")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "z0")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: PDIFF_4:42 (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_pdiff_4 :::"Directiondiff"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k4_pdiff_4 :::"grad"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k5_pdiff_4 :::"unitvector"::: ) (Set (Var "a")) ")" ) ($#k23_rvsum_1 :::")|"::: ) )))) ; definitionlet "f1", "f2", "f3" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)); func :::"curl"::: "(" "f1" "," "f2" "," "f3" "," "p" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) equals :: PDIFF_4:def 10 (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f3" "," "p" "," (Num 2) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f2" "," "p" "," (Num 3) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f1" "," "p" "," (Num 3) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f3" "," "p" "," (Num 1) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f2" "," "p" "," (Num 1) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" "f1" "," "p" "," (Num 2) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" )); end; :: deftheorem defines :::"curl"::: PDIFF_4:def 10 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) "holds" (Bool (Set ($#k7_pdiff_4 :::"curl"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f3")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k2_euclid_8 :::""::: ) ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f3")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k3_euclid_8 :::""::: ) ) ")" ) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ")" ) ($#k9_euclid :::"*"::: ) (Set ($#k4_euclid_8 :::""::: ) ) ")" ))))); theorem :: PDIFF_4:43 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 3)) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 3) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k7_pdiff_4 :::"curl"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_8 :::"|["::: ) (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f3")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "p")) "," (Num 3) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f3")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "p")) "," (Num 1) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "p")) "," (Num 2) ")" ")" ) ")" ) ($#k1_euclid_8 :::"]|"::: ) )))) ;