:: CC0SP1 semantic presentation begin definitionlet "V" be ($#l1_cfuncdom :::"ComplexAlgebra":::); mode :::"ComplexSubAlgebra"::: "of" "V" -> ($#l1_cfuncdom :::"ComplexAlgebra":::) means :: CC0SP1:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "V") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "V") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" "V") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "V")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) ")" ); end; :: deftheorem defines :::"ComplexSubAlgebra"::: CC0SP1:def 1 : (Bool "for" (Set (Var "V")) "," (Set (Var "b2")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set (Var "V"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) & (Bool (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "V")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ) ")" )); theorem :: CC0SP1:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X")) (Bool "for" (Set (Var "MR")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "V1")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "V")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set (Var "V1")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set (Var "V1")))) & (Bool (Set (Var "MR")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "V1")) "is" ($#v1_c0sp1 :::"having-inverse"::: ) )) "holds" (Bool (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set (Var "X")) "," (Set (Var "M")) "," (Set (Var "A")) "," (Set (Var "MR")) "," (Set (Var "d2")) "," (Set (Var "d1")) "#)" ) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set (Var "V")))))))))) ; registrationlet "V" be ($#l1_cfuncdom :::"ComplexAlgebra":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_clvect_1 :::"vector-distributive"::: ) ($#v3_clvect_1 :::"scalar-distributive"::: ) ($#v4_clvect_1 :::"scalar-associative"::: ) ($#v1_cfuncdom :::"strict"::: ) ($#v2_cfuncdom :::"vector-associative"::: ) for ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" "V"; end; definitionlet "V" be ($#l1_cfuncdom :::"ComplexAlgebra":::); let "V1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is :::"Cadditively-linearly-closed"::: means :: CC0SP1:def 2 (Bool "(" (Bool "V1" "is" ($#v1_ideal_1 :::"add-closed"::: ) ) & (Bool "V1" "is" ($#v1_c0sp1 :::"having-inverse"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "V1")) "holds" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) "V1")) ")" ) ")" ); end; :: deftheorem defines :::"Cadditively-linearly-closed"::: CC0SP1:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v1_ideal_1 :::"add-closed"::: ) ) & (Bool (Set (Var "V1")) "is" ($#v1_c0sp1 :::"having-inverse"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) ")" ) ")" ) ")" ))); definitionlet "V" be ($#l1_cfuncdom :::"ComplexAlgebra":::); let "V1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume (Bool "(" (Bool (Set (Const "V1")) "is" ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Const "V1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ; func :::"Mult_"::: "(" "V1" "," "V" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," "V1" ($#k2_zfmisc_1 :::":]"::: ) ) "," "V1" equals :: CC0SP1:def 3 (Set (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" "V") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," "V1" ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"Mult_"::: CC0SP1:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Var "V1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) ))))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexBoundedFunctions"::: "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) equals :: CC0SP1:def 4 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) "X") "is" ($#v1_comseq_2 :::"bounded"::: ) ) "}" ; end; :: deftheorem defines :::"ComplexBoundedFunctions"::: CC0SP1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) : (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) "}" )); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_cfuncdom :::"CAlgebra"::: ) "X") -> ($#v5_clvect_1 :::"scalar-unital"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_c0sp1 :::"multiplicatively-closed"::: ) ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ; end; registrationlet "V" be ($#l1_cfuncdom :::"ComplexAlgebra":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_c0sp1 :::"multiplicatively-closed"::: ) ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")); end; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_clvect_1 :::"CLSStruct"::: ) ; attr "V" is :::"scalar-mult-cancelable"::: means :: CC0SP1:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) ")" ))); end; :: deftheorem defines :::"scalar-mult-cancelable"::: CC0SP1:def 5 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_clvect_1 :::"CLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v2_cc0sp1 :::"scalar-mult-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ")" )); theorem :: CC0SP1:2 (Bool "for" (Set (Var "V")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_c0sp1 :::"multiplicatively-closed"::: ) ($#v1_cc0sp1 :::"Cadditively-linearly-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "#)" ) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set (Var "V"))))) ; theorem :: CC0SP1:3 (Bool "for" (Set (Var "V")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w"))))) ")" ) & (Bool "(" "for" (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set (Var "v1")) ($#k8_group_1 :::"*"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_group_1 :::"*"::: ) (Set (Var "w"))))) ")" ) & (Bool "(" "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v")))))) ")" ) & (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "V1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "V")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"C_Algebra_of_BoundedFunctions"::: "X" -> ($#l1_cfuncdom :::"ComplexAlgebra":::) equals :: CC0SP1:def 6 (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"C_Algebra_of_BoundedFunctions"::: CC0SP1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "#)" ))); theorem :: CC0SP1:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X"))) "is" ($#m1_cc0sp1 :::"ComplexSubAlgebra"::: ) "of" (Set ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) "X") -> ($#v5_clvect_1 :::"scalar-unital"::: ) ; end; theorem :: CC0SP1:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "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 (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")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP1:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "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")))) "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")) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))))) ; theorem :: CC0SP1:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "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 (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")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP1:8 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: CC0SP1:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k3_cc0sp1 :::"C_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_complex1 :::"1r"::: ) )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "F")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Const "X")))) ; func :::"modetrans"::: "(" "F" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: CC0SP1:def 7 (Bool "(" (Bool it ($#r1_hidden :::"="::: ) "F") & (Bool (Set it ($#k2_partfun1 :::"|"::: ) "X") "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ); end; :: deftheorem defines :::"modetrans"::: CC0SP1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_cc0sp1 :::"modetrans"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "b3")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"PreNorms"::: "f" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: CC0SP1:def 8 "{" (Set ($#k17_complex1 :::"|."::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool verum) "}" ; end; :: deftheorem defines :::"PreNorms"::: CC0SP1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k5_cc0sp1 :::"PreNorms"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool verum) "}" ))); theorem :: CC0SP1:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k5_cc0sp1 :::"PreNorms"::: ) (Set (Var "f"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ))) ; theorem :: CC0SP1:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) "iff" (Bool (Set ($#k5_cc0sp1 :::"PreNorms"::: ) (Set (Var "f"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexBoundedFunctionsNorm"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: CC0SP1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X"))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k5_cc0sp1 :::"PreNorms"::: ) (Set "(" ($#k4_cc0sp1 :::"modetrans"::: ) "(" (Set (Var "x")) "," "X" ")" ")" ) ")" )))); end; :: deftheorem defines :::"ComplexBoundedFunctionsNorm"::: CC0SP1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k5_cc0sp1 :::"PreNorms"::: ) (Set "(" ($#k4_cc0sp1 :::"modetrans"::: ) "(" (Set (Var "x")) "," (Set (Var "X")) ")" ")" ) ")" )))) ")" ))); theorem :: CC0SP1:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k4_cc0sp1 :::"modetrans"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: CC0SP1:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set (Var "X")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k5_cc0sp1 :::"PreNorms"::: ) (Set (Var "f")) ")" ))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"C_Normed_Algebra_of_BoundedFunctions"::: "X" -> ($#l1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) equals :: CC0SP1:def 10 (Set ($#g1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) "X" ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"C_Normed_Algebra_of_BoundedFunctions"::: CC0SP1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) "(#" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k6_cc0sp1 :::"ComplexBoundedFunctionsNorm"::: ) (Set (Var "X")) ")" ) "#)" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) "X") -> ($#v1_group_1 :::"unital"::: ) ; end; theorem :: CC0SP1:14 (Bool "for" (Set (Var "W")) "being" ($#l1_clopban2 :::"Normed_Complex_AlgebraStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_cfuncdom :::"ComplexAlgebra":::) "st" (Bool (Bool (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_clvect_1 :::"Mult"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "W"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "W")) "is" ($#l1_cfuncdom :::"ComplexAlgebra":::)))) ; theorem :: CC0SP1:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X"))) "is" ($#l1_cfuncdom :::"ComplexAlgebra":::))) ; theorem :: CC0SP1:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cc0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k2_cc0sp1 :::"ComplexBoundedFunctions"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k6_complex1 :::"1r"::: ) ) "," (Set (Var "F")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: CC0SP1:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X"))) "is" ($#l1_clvect_1 :::"ComplexLinearSpace":::))) ; theorem :: CC0SP1:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" )))) ; theorem :: CC0SP1:19 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))))) ; theorem :: CC0SP1:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))) ; theorem :: CC0SP1:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))) ; theorem :: CC0SP1:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "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 "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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")) ($#k1_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")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP1:23 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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")) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))))) ; theorem :: CC0SP1:24 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "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 "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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")) ($#k6_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")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP1:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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 "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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 ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k11_binop_2 :::"*"::: ) (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 :::".||"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "G")) ($#k1_normsp_0 :::".||"::: ) ))) ")" )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) "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 :: CC0SP1:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "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 "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CC0SP1:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (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 ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) "X") -> ($#v3_clopban1 :::"complete"::: ) ; end; theorem :: CC0SP1:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_cc0sp1 :::"C_Normed_Algebra_of_BoundedFunctions"::: ) (Set (Var "X"))) "is" ($#l1_clopban2 :::"Complex_Banach_Algebra":::))) ;