:: CC0SP2 semantic presentation begin definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); attr "f" is :::"continuous"::: means :: CC0SP2:def 1 (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v5_cfdiff_1 :::"closed"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) "is" ($#v4_pre_topc :::"closed"::: ) )); end; :: deftheorem defines :::"continuous"::: CC0SP2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_cc0sp2 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v5_cfdiff_1 :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))); definitionlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "y" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "X" :::"-->"::: "y" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: CC0SP2:def 2 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#k7_funcop_1 :::"-->"::: ) "y"); end; :: deftheorem defines :::"-->"::: CC0SP2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")))))); theorem :: CC0SP2:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "f")) "is" ($#v1_cc0sp2 :::"continuous"::: ) )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "y" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k1_cc0sp2 :::"-->"::: ) "y") -> ($#v1_cc0sp2 :::"continuous"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) bbbadV1_VALUED_0() ($#v1_cc0sp2 :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: CC0SP2:2 (Bool "for" (Set (Var "X")) "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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_cc0sp2 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v6_cfdiff_1 :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))) ; theorem :: CC0SP2:3 (Bool "for" (Set (Var "X")) "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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_cc0sp2 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) "is" ($#v6_cfdiff_1 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )))) ")" ))) ; theorem :: CC0SP2:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k11_pre_poly :::"+"::: ) (Set (Var "g"))) "is" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) )))) ; theorem :: CC0SP2:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ))))) ; theorem :: CC0SP2:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k46_valued_1 :::"-"::: ) (Set (Var "g"))) "is" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) )))) ; theorem :: CC0SP2:7 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k19_valued_1 :::"(#)"::: ) (Set (Var "g"))) "is" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) )))) ; theorem :: CC0SP2:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"CContinuousFunctions"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) equals :: CC0SP2:def 3 "{" (Set (Var "f")) where f "is" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool verum) "}" ; end; :: deftheorem defines :::"CContinuousFunctions"::: CC0SP2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#v1_cc0sp2 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool verum) "}" )); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X") -> ($#v3_c0sp1 :::"multiplicatively-closed"::: ) ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"C_Algebra_of_ContinuousFunctions"::: "X" -> ($#l1_cfuncdom :::"ComplexAlgebra":::) equals :: CC0SP2:def 4 (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"C_Algebra_of_ContinuousFunctions"::: CC0SP2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "#)" ))); theorem :: CC0SP2:9 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X"))) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v1_cfuncdom :::"strict"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v5_clvect_1 :::"scalar-unital"::: ) ; end; theorem :: CC0SP2:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP2:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))))) ; theorem :: CC0SP2:12 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_group_1 :::"*"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP2:13 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set ($#k5_complex1 :::"0c"::: ) )))) ; theorem :: CC0SP2:14 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set ($#k6_complex1 :::"1r"::: ) )))) ; theorem :: CC0SP2:15 (Bool "for" (Set (Var "A")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A2"))))) "holds" (Bool (Set (Var "A1")) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set (Var "A2"))))) ; theorem :: CC0SP2:16 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k3_cc0sp2 :::"C_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X"))) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); func :::"CContinuousFunctionsNorm"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: CC0SP2:def 5 (Set (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" )); end; :: deftheorem defines :::"CContinuousFunctionsNorm"::: CC0SP2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k4_cc0sp2 :::"CContinuousFunctionsNorm"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" )))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); func :::"C_Normed_Algebra_of_ContinuousFunctions"::: "X" -> ($#l1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) equals :: CC0SP2:def 6 (Set ($#g1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k4_cc0sp2 :::"CContinuousFunctionsNorm"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"C_Normed_Algebra_of_ContinuousFunctions"::: CC0SP2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k4_cc0sp2 :::"CContinuousFunctionsNorm"::: ) (Set (Var "X")) ")" ) "#)" ))); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_clopban2 :::"strict"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v1_group_1 :::"unital"::: ) ; end; theorem :: CC0SP2:17 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X"))) "is" ($#l1_cfuncdom :::"ComplexAlgebra":::))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v2_clvect_1 :::"vector-distributive"::: ) ($#v3_clvect_1 :::"scalar-distributive"::: ) ($#v4_clvect_1 :::"scalar-associative"::: ) ($#v2_cfuncdom :::"vector-associative"::: ) ; end; theorem :: CC0SP2:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k6_complex1 :::"1r"::: ) ) "," (Set (Var "F")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v2_clvect_1 :::"vector-distributive"::: ) ($#v3_clvect_1 :::"scalar-distributive"::: ) ($#v4_clvect_1 :::"scalar-associative"::: ) ($#v5_clvect_1 :::"scalar-unital"::: ) ; end; theorem :: CC0SP2:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X"))) "is" ($#l1_clvect_1 :::"ComplexLinearSpace":::))) ; theorem :: CC0SP2:20 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" )))) ; theorem :: CC0SP2:21 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))) ; theorem :: CC0SP2:22 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP2:23 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))))) ; theorem :: CC0SP2:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_group_1 :::"*"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP2:25 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: CC0SP2:26 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ))))) ; theorem :: CC0SP2:27 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))))) ; theorem :: CC0SP2:28 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "F")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "G")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "G")) ($#k1_normsp_0 :::".||"::: ) ))))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v8_clvect_1 :::"ComplexNormSpace-like"::: ) ; end; theorem :: CC0SP2:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP2:30 (Bool "for" (Set (Var "X")) "being" ($#l2_clvect_1 :::"ComplexBanachSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v2_ncfcont1 :::"closed"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "seq")) "is" ($#v1_csspace3 :::"CCauchy"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set (Var "seq"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )))) ; theorem :: CC0SP2:31 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "Y")) "is" ($#v2_ncfcont1 :::"closed"::: ) ))) ; theorem :: CC0SP2:32 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_csspace3 :::"CCauchy"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v9_clvect_1 :::"convergent"::: ) ))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v3_clopban1 :::"complete"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_cc0sp2 :::"C_Normed_Algebra_of_ContinuousFunctions"::: ) "X") -> ($#v5_clopban2 :::"Banach_Algebra-like"::: ) ; end; theorem :: CC0SP2:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "f")) ($#k11_pre_poly :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "g")) ")" ))))) ; theorem :: CC0SP2:34 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "a")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "f"))))))) ; theorem :: CC0SP2:35 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "f")) ($#k19_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "g")) ")" ))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"CC_0_Functions"::: "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) equals :: CC0SP2:def 7 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_cc0sp2 :::"continuous"::: ) ) & (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))) ")" ) ")" )) ")" ) "}" ; end; :: deftheorem defines :::"CC_0_Functions"::: CC0SP2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_cc0sp2 :::"continuous"::: ) ) & (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))) ")" ) ")" )) ")" ) "}" )); theorem :: CC0SP2:36 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ))) ; theorem :: CC0SP2:37 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "W")) "is" ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ))) ; theorem :: CC0SP2:38 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))) "is" ($#v1_ideal_1 :::"add-closed"::: ) )) ; theorem :: CC0SP2:39 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))) "is" ($#v6_clvect_1 :::"linearly-closed"::: ) )) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_clvect_1 :::"linearly-closed"::: ) ; end; theorem :: CC0SP2:40 (Bool "for" (Set (Var "V")) "being" ($#l1_clvect_1 :::"ComplexLinearSpace":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#v6_clvect_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Var "V1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "#)" ) "is" ($#m1_clvect_1 :::"Subspace"::: ) "of" (Set (Var "V"))))) ; theorem :: CC0SP2:41 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "#)" ) "is" ($#m1_clvect_1 :::"Subspace"::: ) "of" (Set ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"C_VectorSpace_of_C_0_Functions"::: "X" -> ($#l1_clvect_1 :::"ComplexLinearSpace":::) equals :: CC0SP2:def 8 (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"C_VectorSpace_of_C_0_Functions"::: CC0SP2:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k7_cc0sp2 :::"C_VectorSpace_of_C_0_Functions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "#)" ))); theorem :: CC0SP2:42 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"CC_0_FunctionsNorm"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: CC0SP2:def 9 (Set (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" )); end; :: deftheorem defines :::"CC_0_FunctionsNorm"::: CC0SP2:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k8_cc0sp2 :::"CC_0_FunctionsNorm"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" )))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"C_Normed_Space_of_C_0_Functions"::: "X" -> ($#l2_clvect_1 :::"CNORMSTR"::: ) equals :: CC0SP2:def 10 (Set ($#g2_clvect_1 :::"CNORMSTR"::: ) "(#" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) "X" ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ")" ")" ) "," (Set "(" ($#k8_cc0sp2 :::"CC_0_FunctionsNorm"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"C_Normed_Space_of_C_0_Functions"::: CC0SP2:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g2_clvect_1 :::"CNORMSTR"::: ) "(#" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set "(" ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ")" ) "," (Set "(" ($#k8_cc0sp2 :::"CC_0_FunctionsNorm"::: ) (Set (Var "X")) ")" ) "#)" ))); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_clvect_1 :::"strict"::: ) ; end; theorem :: CC0SP2:43 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cc0sp2 :::"CC_0_Functions"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cc0sp2 :::"CContinuousFunctions"::: ) (Set (Var "X")))))) ; theorem :: CC0SP2:44 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_cc0sp2 :::"C_VectorSpace_of_C_0_Functions"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: CC0SP2:45 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_cc0sp2 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: CC0SP2:46 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) (Set (Var "X")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) (Set (Var "X")) ")" )))) "implies" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "F")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "G")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "G")) ($#k1_normsp_0 :::".||"::: ) ))) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) "X") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_clvect_1 :::"vector-distributive"::: ) ($#v3_clvect_1 :::"scalar-distributive"::: ) ($#v4_clvect_1 :::"scalar-associative"::: ) ($#v5_clvect_1 :::"scalar-unital"::: ) ($#v8_clvect_1 :::"ComplexNormSpace-like"::: ) ; end; theorem :: CC0SP2:47 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k9_cc0sp2 :::"C_Normed_Space_of_C_0_Functions"::: ) (Set (Var "X"))) "is" ($#l2_clvect_1 :::"ComplexNormSpace":::))) ;