:: NDIFF_1 semantic presentation begin theorem :: NDIFF_1:1 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "N1"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "N2"))) ")" ))))) ; theorem :: NDIFF_1:2 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "st" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))))))) ; theorem :: NDIFF_1:3 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) "}" ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))))) ; theorem :: NDIFF_1:4 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "st" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) ))) ; theorem :: NDIFF_1:5 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "st" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ")" ) "iff" (Bool (Set (Var "X")) "is" ($#v3_nfcont_1 :::"open"::: ) ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "S")); redefine attr "f" is :::"non-zero"::: means :: NDIFF_1:def 1 (Bool (Set ($#k2_relset_1 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) "S")); end; :: deftheorem defines :::"non-zero"::: NDIFF_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v12_struct_0 :::"non-zero"::: ) ) "iff" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "S")))) ")" )))); theorem :: NDIFF_1:6 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v12_struct_0 :::"non-zero"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) "holds" (Bool (Set (Set (Var "seq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) ")" ))) ; theorem :: NDIFF_1:7 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v12_struct_0 :::"non-zero"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) ")" ))) ; definitionlet "RNS" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); let "a" be ($#m1_subset_1 :::"Real_Sequence":::); func "a" :::"(#)"::: "S" -> ($#m1_subset_1 :::"sequence":::) "of" "RNS" means :: NDIFF_1:def 2 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "S" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"(#)"::: NDIFF_1:def 2 : (Bool "for" (Set (Var "RNS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "S")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); definitionlet "RNS" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "z" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RNS")); let "a" be ($#m1_subset_1 :::"Real_Sequence":::); func "a" :::"*"::: "z" -> ($#m1_subset_1 :::"sequence":::) "of" "RNS" means :: NDIFF_1:def 3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "a" ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_rlvect_1 :::"*"::: ) "z"))); end; :: deftheorem defines :::"*"::: NDIFF_1:def 3 : (Bool "for" (Set (Var "RNS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z"))))) ")" ))))); theorem :: NDIFF_1:8 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "rseq1")) "," (Set (Var "rseq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "rseq1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "rseq2")) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "rseq1")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set (Var "rseq2")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: NDIFF_1:9 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq1")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq2")) ")" )))))) ; theorem :: NDIFF_1:10 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set (Var "r")) ($#k5_normsp_1 :::"*"::: ) (Set "(" (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" (Set (Var "r")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ))))))) ; theorem :: NDIFF_1:11 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "rseq1")) "," (Set (Var "rseq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "rseq1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "rseq2")) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "rseq1")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "rseq2")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: NDIFF_1:12 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq1")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq2")) ")" )))))) ; theorem :: NDIFF_1:13 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v3_normsp_1 :::"convergent"::: ) )))) ; theorem :: NDIFF_1:14 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "rseq")) ($#k1_ndiff_1 :::"(#)"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: NDIFF_1:15 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq1")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: NDIFF_1:16 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq1")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: NDIFF_1:17 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v12_struct_0 :::"non-zero"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v12_struct_0 :::"non-zero"::: ) )))) ; definitionlet "S" be ($#l1_normsp_1 :::"RealNormSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "IT" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "S")); attr "IT" is "x" :::"-convergent"::: means :: NDIFF_1:def 4 (Bool "(" (Bool "IT" "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) "IT") ($#r1_hidden :::"="::: ) "x") ")" ); end; :: deftheorem defines :::"-convergent"::: NDIFF_1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" (Set (Var "x")) ($#v1_ndiff_1 :::"-convergent"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" )))); theorem :: NDIFF_1:18 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ))) ; theorem :: NDIFF_1:19 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x0")))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ))))) ; theorem :: NDIFF_1:20 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x0")))) ")" )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S")))))))) ; registrationlet "S" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); cluster bbbadV1_XBOOLE_0() bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) "S") ($#v1_ndiff_1 :::"-convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))))); end; theorem :: NDIFF_1:21 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "a")) "being" ($#v2_relat_1 :::"non-zero"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v1_fdiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z"))) "is" ($#v12_struct_0 :::"non-zero"::: ) ) & (Bool (Set (Set (Var "a")) ($#k2_ndiff_1 :::"*"::: ) (Set (Var "z"))) "is" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))) ($#v1_ndiff_1 :::"-convergent"::: ) ) ")" )))) ; theorem :: NDIFF_1:22 (Bool "for" (Set (Var "S")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) "iff" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ) ")" ) "iff" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))) ; registrationlet "S" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); cluster bbbadV1_XBOOLE_0() bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))))); end; definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "IT" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "IT" is :::"RestFunc-like"::: means :: NDIFF_1:def 5 (Bool "(" (Bool "IT" "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "(" "for" (Set (Var "h")) "being" ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) "S") ($#v1_ndiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"sequence":::) "of" "S" "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "h")) ($#k4_normsp_0 :::".||"::: ) ) ($#k37_valued_1 :::"""::: ) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" "IT" ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "h")) ($#k4_normsp_0 :::".||"::: ) ) ($#k37_valued_1 :::"""::: ) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" "IT" ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "T")) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"RestFunc-like"::: NDIFF_1:def 5 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_ndiff_1 :::"RestFunc-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "(" "for" (Set (Var "h")) "being" ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b1"))) ($#v1_ndiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "h")) ($#k4_normsp_0 :::".||"::: ) ) ($#k37_valued_1 :::"""::: ) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" (Set (Var "IT")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "h")) ($#k4_normsp_0 :::".||"::: ) ) ($#k37_valued_1 :::"""::: ) ")" ) ($#k1_ndiff_1 :::"(#)"::: ) (Set "(" (Set (Var "IT")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T")))) ")" ) ")" ) ")" ) ")" ))); registrationlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_ndiff_1 :::"RestFunc-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); end; definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); mode RestFunc of "S" "," "T" is ($#v2_ndiff_1 :::"RestFunc-like"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" "S" "," "T"; end; theorem :: NDIFF_1:23 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_ndiff_1 :::"RestFunc-like"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S")))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k2_real_1 :::"""::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))) ")" ))) ; theorem :: NDIFF_1:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "s")) "being" ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b1"))) ($#v1_ndiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s"))) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "R")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T")))) ")" )))) ; theorem :: NDIFF_1:25 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "h1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "h2")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set (Set "(" (Set (Var "h1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; theorem :: NDIFF_1:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "r")) ($#k5_normsp_1 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))))))) ; theorem :: NDIFF_1:27 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_nfcont_1 :::"is_continuous_in"::: ) (Set (Var "x0"))) "iff" (Bool "(" (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "s1")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Var "x0"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "s1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x0"))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s1"))) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s1")) ")" ))) ")" ) ")" ) ")" ) ")" )))) ; theorem :: NDIFF_1:28 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "R1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "R2"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T"))) & (Bool (Set (Set (Var "R1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "R2"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" ))) ; theorem :: NDIFF_1:29 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")))))) ; definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "x0" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); pred "f" :::"is_differentiable_in"::: "x0" means :: NDIFF_1:def 6 (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" "x0" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" "S" "," "T" ")" ")" )(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" "S" "," "T" "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) "x0" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) "x0" ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) "x0" ")" ) ")" )))))) ")" )); end; :: deftheorem defines :::"is_differentiable_in"::: NDIFF_1:def 6 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" )(Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x0")) ")" ) ")" )))))) ")" )) ")" )))); definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "x0" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); assume (Bool (Set (Const "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Const "x0"))) ; func :::"diff"::: "(" "f" "," "x0" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" "S" "," "T" ")" ")" ) means :: NDIFF_1:def 7 (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" "x0" "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" "S" "," "T" "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) "x0" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) "x0" ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) "x0" ")" ) ")" ))))) ")" )); end; :: deftheorem defines :::"diff"::: NDIFF_1:def 7 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" )) "iff" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b5")) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))))) ")" )) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); pred "f" :::"is_differentiable_on"::: "X" means :: NDIFF_1:def 8 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) "X") ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ); end; :: deftheorem defines :::"is_differentiable_on"::: NDIFF_1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ) ")" )))); theorem :: NDIFF_1:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")))))) ; theorem :: NDIFF_1:31 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) "iff" (Bool "(" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) ")" ) ")" )))) ; theorem :: NDIFF_1:32 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) "is" ($#v3_nfcont_1 :::"open"::: ) )))) ; definitionlet "S", "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Const "X"))) ; func "f" :::"`|"::: "X" -> ($#m1_subset_1 :::"PartFunc":::) "of" "S" "," (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" "S" "," "T" ")" ")" ) means :: NDIFF_1:def 9 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" "f" "," (Set (Var "x")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"`|"::: NDIFF_1:def 9 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )) ")" ) ")" ) ")" ))))); theorem :: NDIFF_1:33 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ))) ")" ) ")" )))) ; registrationlet "S" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::); let "h" be ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Const "S"))) ($#v1_ndiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "S")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "h" ($#k9_nat_1 :::"^\"::: ) "n") -> ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) "S") ($#v1_ndiff_1 :::"-convergent"::: ) for ($#m1_subset_1 :::"sequence":::) "of" "S"; end; theorem :: NDIFF_1:34 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#v12_struct_0 :::"non-zero"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b1"))) ($#v1_ndiff_1 :::"-convergent"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "c")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" )) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "c")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T")))) ")" ))))))) ; theorem :: NDIFF_1:35 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "f2")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x0")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x0")) ")" ")" ))) ")" )))) ; theorem :: NDIFF_1:36 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Var "f2")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x0")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x0")) ")" ")" ))) ")" )))) ; theorem :: NDIFF_1:37 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k3_ndiff_1 :::"diff"::: ) "(" (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ))) ")" ))))) ; theorem :: NDIFF_1:38 (Bool "for" (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "S")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "Z"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ) ")" )))) ; theorem :: NDIFF_1:39 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool (Set (Var "f2")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" )))) ; theorem :: NDIFF_1:40 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Var "f1")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool (Set (Var "f2")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f1")) "," (Set (Var "x")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f2")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" )))) ; theorem :: NDIFF_1:41 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" ))))) ; theorem :: NDIFF_1:42 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ))) ")" ) ")" )))) ; theorem :: NDIFF_1:43 (Bool "for" (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k4_ndiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_lopban_2 :::"*"::: ) (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "S")) ")" ))) ")" ) ")" )))))) ; theorem :: NDIFF_1:44 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool (Set (Var "f")) ($#r1_nfcont_1 :::"is_continuous_in"::: ) (Set (Var "x0")))))) ; theorem :: NDIFF_1:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r3_nfcont_1 :::"is_continuous_on"::: ) (Set (Var "X")))))) ; theorem :: NDIFF_1:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v3_nfcont_1 :::"open"::: ) ) & (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r2_ndiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))))))) ; theorem :: NDIFF_1:47 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_ndiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x0")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"RestFunc":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool "(" (Bool (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T")))) & (Bool (Set (Var "R")) ($#r1_nfcont_1 :::"is_continuous_in"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_ndiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ) ($#k17_lopban_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ))) ")" ) ")" )) ")" ))))) ;