:: TIETZE  semantic presentation begin  











theorem :: TIETZE:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))  ")" )) ; 
 
theorem :: TIETZE:2 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "h"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "h"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "g"))))) ; 
 
theorem :: TIETZE:3 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "h")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "g"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "h"))))) ; 
 definitionlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; pred "f" "," "X" :::"is_absolutely_bounded_by"::: "r" means :: TIETZE:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set "X"  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "f" ")" )))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  "r")); end; 






:: deftheorem    defines :::"is_absolutely_bounded_by"::: TIETZE:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))))  ")" )))); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_funct_1 :::"constant"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_valued_0 :::"ext-real-valued"::: )     ($#v3_valued_0 :::"real-valued"::: )     ($#v1_series_1 :::"summable"::: )     ($#v2_comseq_2 :::"convergent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; 
theorem :: TIETZE:4 (Bool  "for" (Set (Var "T1")) "being"   ($#v2_struct_0 :::"empty"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 
theorem :: TIETZE:5 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_series_1 :::"summable"::: )    ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "g"))))) ; 
 
theorem :: TIETZE:6 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_series_1 :::"absolutely_summable"::: )  )) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set (Var "f")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: TIETZE:7 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "f")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: TIETZE:8 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) ")" ))) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) ")" )))  ")" ))) ; 
 
theorem :: TIETZE:9 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_seqfunc :::"common_on_dom"::: )  (Set (Var "F")))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set (Var "n")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) "," (Set (Var "Z"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "F"))  ($#r3_seqfunc :::"is_unif_conv_on"::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k11_seqfunc :::"lim"::: )   "(" (Set (Var "F")) "," (Set (Var "Z")) ")"  ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set (Var "n")) ")" )) "," (Set (Var "Z"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: TIETZE:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_seqfunc :::"common_on_dom"::: )  (Set (Var "F")))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set (Var "n")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) "," (Set (Var "Z"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "Z")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k11_seqfunc :::"lim"::: )   "(" (Set (Var "F")) "," (Set (Var "Z")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "z")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) ")" ))) & (Bool (Set (Set  "("  ($#k11_seqfunc :::"lim"::: )   "(" (Set (Var "F")) "," (Set (Var "Z")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "z")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) ")" )))  ")" ))))) ; 
 
theorem :: TIETZE:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_seqfunc :::"common_on_dom"::: )  (Set (Var "F")))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Z")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set (Var "n")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set (Var "f"))) "," (Set (Var "Z"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "F"))  ($#r2_seqfunc :::"is_point_conv_on"::: )  (Set (Var "Z"))) & (Bool (Set   ($#k11_seqfunc :::"lim"::: )   "(" (Set (Var "F")) "," (Set (Var "Z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "f")))  ")" ))))) ; 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "A") ->   ($#v1_borsuk_1 :::"closed"::: )   ; 
end; 
theorem :: TIETZE:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))  "st" (Bool (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_tsep_1 :::"misses"::: )  (Set (Var "X2"))) "or" (Bool (Set (Set (Var "f1"))  ($#k3_tmap_1 :::"|"::: )  (Set  "(" (Set (Var "X1"))  ($#k2_tsep_1 :::"meet"::: )  (Set (Var "X2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f2"))  ($#k3_tmap_1 :::"|"::: )  (Set  "(" (Set (Var "X1"))  ($#k2_tsep_1 :::"meet"::: )  (Set (Var "X2")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X1"))))) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k10_tmap_1 :::"union"::: )  (Set (Var "f2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X2"))))) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k10_tmap_1 :::"union"::: )  (Set (Var "f2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")"   ")" )))))) ; 
 
theorem :: TIETZE:13 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))  "st" (Bool (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_tsep_1 :::"misses"::: )  (Set (Var "X2"))) "or" (Bool (Set (Set (Var "f1"))  ($#k3_tmap_1 :::"|"::: )  (Set  "(" (Set (Var "X1"))  ($#k2_tsep_1 :::"meet"::: )  (Set (Var "X2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f2"))  ($#k3_tmap_1 :::"|"::: )  (Set  "(" (Set (Var "X1"))  ($#k2_tsep_1 :::"meet"::: )  (Set (Var "X2")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "f1"))  ($#k10_tmap_1 :::"union"::: )  (Set (Var "f2")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f1")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f2")) ")" ))))))) ; 
 
theorem :: TIETZE:14 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))  "st" (Bool (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_tsep_1 :::"misses"::: )  (Set (Var "X2"))) "or" (Bool (Set (Set (Var "f1"))  ($#k3_tmap_1 :::"|"::: )  (Set  "(" (Set (Var "X1"))  ($#k2_tsep_1 :::"meet"::: )  (Set (Var "X2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f2"))  ($#k3_tmap_1 :::"|"::: )  (Set  "(" (Set (Var "X1"))  ($#k2_tsep_1 :::"meet"::: )  (Set (Var "X2")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k10_tmap_1 :::"union"::: )  (Set (Var "f2")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k10_tmap_1 :::"union"::: )  (Set (Var "f2")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))))  ")" )  ")" ))))) ; 
 
theorem :: TIETZE:15 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g"))) & (Bool (Set (Var "g")) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "f")) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))))) ; 
 
theorem :: TIETZE:16 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) "or" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))  ")" ) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))) & (Bool (Set (Var "f")) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "g")) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))))) ; 
 






theorem :: TIETZE:17 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "T")) "is"   ($#v10_pre_topc :::"normal"::: )  )) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "A"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "g")) "," (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Set (Var "r"))  ($#k6_real_1 :::"/"::: )  (Num 3))) & (Bool (Set (Set (Var "f"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "g"))) "," (Set (Var "A"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" )  ($#k10_real_1 :::"/"::: )  (Num 3)))  ")" )))))) ; 
 
theorem :: TIETZE:18 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_subset_1 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))  ")" ))  ")" )) "holds"  (Bool (Set (Var "T")) "is"   ($#v10_pre_topc :::"normal"::: )  )) ; 
 
theorem :: TIETZE:19 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_tmap_1 :::"is_continuous_at"::: )  (Set (Var "x"))) "iff" (Bool  "for" (Set (Var "e")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "H"))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "H")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))  ")" )))) ; 
 
theorem :: TIETZE:20 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "F"))  ($#r3_seqfunc :::"is_unif_conv_on"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_seqfunc :::"."::: )  (Set (Var "i"))) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ))  ")" )) "holds"  (Bool (Set   ($#k11_seqfunc :::"lim"::: )   "(" (Set (Var "F")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )))) ; 
 
theorem :: TIETZE:21 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#v2_xxreal_0 :::"positive"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r"))) "iff" (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "r")) ")"  ")" ))  ")" )))) ; 
 
theorem :: TIETZE:22 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "g"))) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f"))) "," (Set (Var "X"))  ($#r1_tietze :::"is_absolutely_bounded_by"::: )  (Set (Var "r")))))) ; 
 
theorem :: TIETZE:23 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v10_pre_topc :::"normal"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "st" (Bool (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))))) ; 
 
theorem :: TIETZE:24 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) (Bool  "ex" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "st" (Bool (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))))  ")" )) "holds"  (Bool (Set (Var "T")) "is"   ($#v10_pre_topc :::"normal"::: )  )) ;