:: PDIFF_1 semantic presentation begin definitionlet "i", "n" be ($#m1_hidden :::"Nat":::); func :::"proj"::: "(" "i" "," "n" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PDIFF_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) "i"))); end; :: deftheorem defines :::"proj"::: PDIFF_1:def 1 : (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) ")" ))); theorem :: PDIFF_1:1 (Bool "(" (Bool "(" "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n")))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ")" ) ")" ) ")" ) ; theorem :: PDIFF_1:2 (Bool "(" (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" )) & (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Num 1))) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" )) ")" ) ; registration cluster (Set ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ) -> ($#v3_funct_2 :::"bijective"::: ) ; end; definitionlet "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"<>*"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) equals :: PDIFF_1:def 2 (Set (Set "(" (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "g" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" )); end; :: deftheorem defines :::"<>*"::: PDIFF_1:def 2 : (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"<>*"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) equals :: PDIFF_1:def 3 (Set (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "g"); end; :: deftheorem defines :::"<>*"::: PDIFF_1:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))))); definitionlet "i", "n" be ($#m1_hidden :::"Nat":::); func :::"Proj"::: "(" "i" "," "n" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) means :: PDIFF_1:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "i" "," "n" ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))); end; :: deftheorem defines :::"Proj"::: PDIFF_1:def 4 : (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ))); definitionlet "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"reproj"::: "(" "i" "," "x" ")" -> ($#m1_hidden :::"Function":::) means :: PDIFF_1:def 5 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_7 :::"Replace"::: ) "(" "x" "," "i" "," (Set (Var "r")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"reproj"::: PDIFF_1:def 5 : (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "r")) ")" )) ")" ) ")" ) ")" )))); definitionlet "n", "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"reproj"::: redefine func :::"reproj"::: "(" "i" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ); end; definitionlet "n", "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); func :::"reproj"::: "(" "i" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" ) means :: PDIFF_1:def 6 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) "x") & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" "i" "," (Set (Var "y")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) ")" )))); end; :: deftheorem defines :::"reproj"::: PDIFF_1:def 6 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q")))) ")" )))) ")" )))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); pred "f" :::"is_differentiable_in"::: "x" means :: PDIFF_1:def 7 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "st" (Bool "(" (Bool "f" ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "g")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "y"))) ")" ))); end; :: deftheorem defines :::"is_differentiable_in"::: PDIFF_1:def 7 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "g")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "y"))) ")" ))) ")" )))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); assume (Bool (Set (Const "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Const "x"))) ; func :::"diff"::: "(" "f" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "m" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) means :: PDIFF_1:def 8 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "st" (Bool "(" (Bool "f" ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) ")" )) ")" ))); end; :: deftheorem defines :::"diff"::: PDIFF_1:def 8 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) ")" )) ")" ))) ")" ))))); theorem :: PDIFF_1:3 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "y"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "y")) ")" ))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" )))) ")" ) ")" )) ; theorem :: PDIFF_1:4 (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "J")) ($#r2_funct_2 :::"="::: ) (Set ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "y"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "y")))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "a"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "J")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b"))))) ")" ) ")" )) ; theorem :: PDIFF_1:5 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) )) & (Bool (Set (Var "J")) ($#r2_funct_2 :::"="::: ) (Set ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k1_partfun1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "I"))) "is" ($#m1_subset_1 :::"RestFunc":::)) ")" ) & (Bool "(" "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k1_partfun1 :::"*"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "I"))) "is" ($#m1_subset_1 :::"LinearFunc":::)) ")" ) ")" ))) ; theorem :: PDIFF_1:6 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) )) & (Bool (Set (Var "J")) ($#r2_funct_2 :::"="::: ) (Set ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k1_partfun1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "J"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" )) ")" ) & (Bool "(" "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LinearFunc":::) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k1_partfun1 :::"*"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "J"))) "is" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" )) ")" ) ")" ))) ; theorem :: PDIFF_1:7 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Num 1))) ")" ))))) ; theorem :: PDIFF_1:8 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "g")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ")" ))))) ; theorem :: PDIFF_1:9 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "g")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y"))) ")" ))))) ; theorem :: PDIFF_1:10 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))) ; begin definitionlet "n", "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ); pred "f" :::"is_partial_differentiable_in"::: "x" "," "i" means :: PDIFF_1:def 9 (Bool (Set "f" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" "i" "," "x" ")" ")" )) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" "i" "," "m" ")" ")" ) ($#k3_funct_2 :::"."::: ) "x")); end; :: deftheorem defines :::"is_partial_differentiable_in"::: PDIFF_1:def 9 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ))))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ); func :::"partdiff"::: "(" "f" "," "x" "," "i" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" ) ")" ")" ) equals :: PDIFF_1:def 10 (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" "f" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" "i" "," "x" ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" "i" "," "m" ")" ")" ) ($#k3_funct_2 :::"."::: ) "x" ")" ) ")" ); end; :: deftheorem defines :::"partdiff"::: PDIFF_1:def 10 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool (Set ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))); definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_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"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); pred "f" :::"is_partial_differentiable_in"::: "x" "," "i" means :: PDIFF_1:def 11 (Bool (Set "f" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" "i" "," "x" ")" ")" )) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "i" "," "n" ")" ")" ) ($#k1_seq_1 :::"."::: ) "x")); end; :: deftheorem defines :::"is_partial_differentiable_in"::: PDIFF_1:def 11 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_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 "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ))))); definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_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"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); func :::"partdiff"::: "(" "f" "," "x" "," "i" ")" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: PDIFF_1:def 12 (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" "f" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" "i" "," "x" ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "i" "," "n" ")" ")" ) ($#k1_seq_1 :::"."::: ) "x" ")" ) ")" ); end; :: deftheorem defines :::"partdiff"::: PDIFF_1:def 12 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_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 "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k10_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))); definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_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"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"partdiff"::: redefine func :::"partdiff"::: "(" "f" "," "x" "," "i" ")" -> ($#m1_subset_1 :::"Real":::); end; theorem :: PDIFF_1:11 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ))))) ; theorem :: PDIFF_1:12 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Num 1) "," (Num 1) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" )))))) ; theorem :: PDIFF_1:13 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "y")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ))))))))) ; theorem :: PDIFF_1:14 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) "iff" (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) ")" ))))))) ; theorem :: PDIFF_1:15 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "f")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))))) ; definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); pred "f" :::"is_partial_differentiable_in"::: "x" "," "i" means :: PDIFF_1:def 13 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "st" (Bool "(" (Bool "f" ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "g")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," "i") ")" ))); end; :: deftheorem defines :::"is_partial_differentiable_in"::: PDIFF_1:def 13 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "g")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) ")" ))) ")" ))))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); assume (Bool (Set (Const "f")) ($#r4_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Const "x")) "," (Set (Const "i"))) ; func :::"partdiff"::: "(" "f" "," "x" "," "i" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") means :: PDIFF_1:def 14 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "st" (Bool "(" (Bool "f" ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) "," "i" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ))); end; :: deftheorem defines :::"partdiff"::: PDIFF_1:def 14 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r4_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k12_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) ")" ))) ")" )))))); theorem :: PDIFF_1:16 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) "iff" (Bool (Set (Var "G")) ($#r4_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) ")" ))))))) ; theorem :: PDIFF_1:17 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "F")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "G")) "," (Set (Var "y")) "," (Set (Var "i")) ")" )))))))) ; theorem :: PDIFF_1:18 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "st" (Bool (Bool (Set (Var "g1")) ($#r2_relset_1 :::"="::: ) (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Var "g1")) ($#r4_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) "iff" (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) ")" )))))) ; theorem :: PDIFF_1:19 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 1) ")" ) "st" (Bool (Bool (Set (Var "g1")) ($#r2_relset_1 :::"="::: ) (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "g")))) & (Bool (Set (Var "g1")) ($#r4_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i")))) "holds" (Bool (Set ($#k12_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; begin definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i", "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ); pred "f" :::"is_partial_differentiable_in"::: "x" "," "i" "," "j" means :: PDIFF_1:def 15 (Bool (Set (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" "j" "," "n" ")" ")" ) ($#k1_partfun1 :::"*"::: ) "f" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" "i" "," "x" ")" ")" )) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" "i" "," "m" ")" ")" ) ($#k3_funct_2 :::"."::: ) "x")); end; :: deftheorem defines :::"is_partial_differentiable_in"::: PDIFF_1:def 15 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r5_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "j"))) "iff" (Bool (Set (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "j")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ))))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i", "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ); func :::"partdiff"::: "(" "f" "," "x" "," "i" "," "j" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) ")" ")" ) equals :: PDIFF_1:def 16 (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" "j" "," "n" ")" ")" ) ($#k1_partfun1 :::"*"::: ) "f" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" "i" "," "x" ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" "i" "," "m" ")" ")" ) ($#k3_funct_2 :::"."::: ) "x" ")" ) ")" ); end; :: deftheorem defines :::"partdiff"::: PDIFF_1:def 16 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool (Set ($#k13_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "j")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i", "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "h" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); pred "h" :::"is_partial_differentiable_in"::: "z" "," "i" "," "j" means :: PDIFF_1:def 17 (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "j" "," "n" ")" ")" ) ($#k1_partfun1 :::"*"::: ) "h" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" "i" "," "z" ")" ")" )) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "i" "," "m" ")" ")" ) ($#k1_seq_1 :::"."::: ) "z")); end; :: deftheorem defines :::"is_partial_differentiable_in"::: PDIFF_1:def 17 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r6_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z")) "," (Set (Var "i")) "," (Set (Var "j"))) "iff" (Bool (Set (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "j")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "z")) ")" ")" )) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z")))) ")" ))))); definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i", "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "h" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "m"))); func :::"partdiff"::: "(" "h" "," "z" "," "i" "," "j" ")" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: PDIFF_1:def 18 (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "j" "," "n" ")" ")" ) ($#k1_partfun1 :::"*"::: ) "h" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" "i" "," "z" ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" "i" "," "m" ")" ")" ) ($#k1_seq_1 :::"."::: ) "z" ")" ) ")" ); end; :: deftheorem defines :::"partdiff"::: PDIFF_1:def 18 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "holds" (Bool (Set ($#k14_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "h")) "," (Set (Var "z")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "j")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "z")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "z")) ")" ) ")" )))))); theorem :: PDIFF_1:20 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "G")) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "y"))) ")" )))))) ; theorem :: PDIFF_1:21 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "F")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_pdiff_1 :::"diff"::: ) "(" (Set (Var "G")) "," (Set (Var "y")) ")" ))))))) ; theorem :: PDIFF_1:22 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_pdiff_1 :::"Proj"::: ) "(" (Set (Var "j")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pdiff_1 :::"<>*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_pdiff_1 :::"proj"::: ) "(" (Set (Var "j")) "," (Set (Var "n")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "z")) ")" ")" ) ")" ))))))))) ; theorem :: PDIFF_1:23 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r5_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "j"))) "iff" (Bool (Set (Var "h")) ($#r6_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "z")) "," (Set (Var "i")) "," (Set (Var "j"))) ")" ))))))) ; theorem :: PDIFF_1:24 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "m"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "f")) ($#r5_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k13_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" ($#k14_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "h")) "," (Set (Var "z")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k9_finseq_1 :::"*>"::: ) )))))))) ; definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); let "X" be ($#m1_hidden :::"set"::: ) ; pred "f" :::"is_partial_differentiable_on"::: "X" "," "i" means :: PDIFF_1:def 19 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "X") ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," "i") ")" ) ")" ); end; :: deftheorem defines :::"is_partial_differentiable_on"::: PDIFF_1:def 19 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) ")" ) ")" ) ")" ))))); theorem :: PDIFF_1:25 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" )))))) ; definitionlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Const "n")) ")" ); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: ) (Set (Const "X")) "," (Set (Const "i"))) ; func "f" :::"`partial|"::: "(" "X" "," "i" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "," (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "n" ")" ) ")" ")" ) means :: PDIFF_1:def 20 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) "m" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_pdiff_1 :::"partdiff"::: ) "(" "f" "," (Set (Var "x")) "," "i" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`partial|"::: PDIFF_1:def 20 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: ) (Set (Var "X")) "," (Set (Var "i")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k15_pdiff_1 :::"`partial|"::: ) "(" (Set (Var "X")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b6")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" )) ")" ) ")" ) ")" )))))); theorem :: PDIFF_1:26 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" ))) ")" ))))) ; theorem :: PDIFF_1:27 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pdiff_1 :::"reproj"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" )))))))) ; theorem :: PDIFF_1:28 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set (Var "f2")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ))) ")" ))))) ; theorem :: PDIFF_1:29 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "g1")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) & (Bool (Set (Var "g2")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "g1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g2"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "g1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g2")) ")" ) "," (Set (Var "y")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g2")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ))) ")" ))))) ; theorem :: PDIFF_1:30 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set (Var "f2")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ))) ")" ))))) ; theorem :: PDIFF_1:31 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "g1")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) & (Bool (Set (Var "g2")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "g1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g2"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "g1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g2")) ")" ) "," (Set (Var "y")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g1")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g2")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ))) ")" ))))) ; theorem :: PDIFF_1:32 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "x")) "," (Set (Var "i"))) & (Bool (Set ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k9_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "i")) ")" ")" ))) ")" )))))) ; theorem :: PDIFF_1:33 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "g")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "y")) "," (Set (Var "i"))) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set (Var "y")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "g")) "," (Set (Var "y")) "," (Set (Var "i")) ")" ")" ))) ")" )))))) ;