:: PDIFF_8  semantic presentation begin  
theorem :: PDIFF_8:1 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))))) ; 
 
theorem :: PDIFF_8:2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "vx")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" )  "st" (Bool (Bool (Set (Var "vx"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "vx")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))))) ; 
 
theorem :: PDIFF_8:3 (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 "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))))) ; 
 
theorem :: PDIFF_8:4 (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 "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ))))) ; 
 
theorem :: PDIFF_8:5 (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 "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))))) ; 
 
theorem :: PDIFF_8:6 (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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set   ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")" ) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" )) & (Bool (Set (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )))) ; 
 
theorem :: PDIFF_8: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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "s"))) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )) & (Bool (Set (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "s")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "s")) ")" )))  ")" )))) ; 
 
theorem :: PDIFF_8:8 (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")) ")" ) "is"   ($#v1_lopban_1 :::"homogeneous"::: )  ))) ; 
 
theorem :: PDIFF_8:9 (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 "x")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k9_euclid :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))))) ; 
 
theorem :: PDIFF_8:10 (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 "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k7_euclid :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "y")) ")" )))))) ; 
 
theorem :: PDIFF_8: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 "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" )))))) ; 
 
theorem :: PDIFF_8: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 "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k8_euclid :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "y")) ")" )))))) ; 
 
theorem :: PDIFF_8: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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "si")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  "st" (Bool (Bool (Set (Var "si"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "si")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "s")) ($#k1_normsp_0 :::".||"::: ) )))))) ; 
 
theorem :: PDIFF_8: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 "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "si")) "," (Set (Var "ti")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "si"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Set (Var "ti"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "t")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "si"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "ti")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "s"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "t")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))))) ; 
 
theorem :: PDIFF_8:15 (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K")))  ")" )) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "s")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "K"))))))) ; 
 
theorem :: PDIFF_8:16 (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::)  (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 "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "s")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K")))  ")" )) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "s")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "K"))))))) ; 
 
theorem :: PDIFF_8:17 (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::)  (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 "s")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k1_pdiff_1 :::"proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K")))  ")" )) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "s")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "K"))))))) ; 
 
theorem :: PDIFF_8: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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "si")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  "st" (Bool (Bool (Set (Var "si"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "si")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))))  ")" )) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "s")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "K"))))))) ; 
 
theorem :: PDIFF_8: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 "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "n")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "si")) "," (Set (Var "ti")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" ) "," (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Num 1) ")" ) ")"  ")" )  "st" (Bool (Bool (Set (Var "si"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Set (Var "ti"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "t")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "si"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "ti")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))))  ")" )) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "s"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "t")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "K"))))))) ; 
 
theorem :: PDIFF_8: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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "X")) "is"   ($#v3_nfcont_1 :::"open"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "f"))  ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k15_pdiff_1 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" ) "iff" (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "j")) "," (Set (Var "n")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "j")) "," (Set (Var "n")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k15_pdiff_1 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" ))  ")" ))))) ; 
 
theorem :: PDIFF_8: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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_nfcont_1 :::"open"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "X")))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" ) "iff" (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "j")) "," (Set (Var "n")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_ndiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Set  "(" (Set  "("  ($#k4_pdiff_1 :::"Proj"::: )   "(" (Set (Var "j")) "," (Set (Var "n")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "X")))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" ))  ")" )))) ; 
 
theorem :: PDIFF_8: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 "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 :::"Subset":::) "of" (Set  "("  ($#k4_real_ns1 :::"REAL-NS"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_nfcont_1 :::"open"::: )  )) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r7_pdiff_1 :::"is_partial_differentiable_on"::: )  (Set (Var "X")) "," (Set (Var "i"))) & (Bool (Set (Set (Var "f"))  ($#k15_pdiff_1 :::"`partial|"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )  ")" ) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_ndiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k4_ndiff_1 :::"`|"::: )  (Set (Var "X")))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set (Var "X")))  ")" )  ")" )))) ;