:: CC0SP2 semantic presentation begin definition let X be TopStruct ; let f be Function of the carrier of X,COMPLEX; attrf is continuous means :Def1: :: CC0SP2:def 1 for Y being Subset of COMPLEX st Y is closed holds f " Y is closed ; end; :: deftheorem Def1 defines continuous CC0SP2:def_1_:_ for X being TopStruct for f being Function of the carrier of X,COMPLEX holds ( f is continuous iff for Y being Subset of COMPLEX st Y is closed holds f " Y is closed ); definition let X be 1-sorted ; let y be complex number ; funcX --> y -> Function of the carrier of X,COMPLEX equals :: CC0SP2:def 2 the carrier of X --> y; coherence the carrier of X --> y is Function of the carrier of X,COMPLEX proof y in COMPLEX by XCMPLX_0:def_2; hence the carrier of X --> y is Function of the carrier of X,COMPLEX by FUNCOP_1:45; ::_thesis: verum end; end; :: deftheorem defines --> CC0SP2:def_2_:_ for X being 1-sorted for y being complex number holds X --> y = the carrier of X --> y; theorem Th1: :: CC0SP2:1 for X being non empty TopSpace for y being complex number for f being Function of the carrier of X,COMPLEX st f = X --> y holds f is continuous proof let X be non empty TopSpace; ::_thesis: for y being complex number for f being Function of the carrier of X,COMPLEX st f = X --> y holds f is continuous let y be complex number ; ::_thesis: for f being Function of the carrier of X,COMPLEX st f = X --> y holds f is continuous let f be Function of the carrier of X,COMPLEX; ::_thesis: ( f = X --> y implies f is continuous ) assume A1: f = X --> y ; ::_thesis: f is continuous set H = the carrier of X; set HX = [#] X; let P1 be Subset of COMPLEX; :: according to CC0SP2:def_1 ::_thesis: ( P1 is closed implies f " P1 is closed ) assume P1 is closed ; ::_thesis: f " P1 is closed percases ( y in P1 or not y in P1 ) ; suppose y in P1 ; ::_thesis: f " P1 is closed then f " P1 = [#] X by A1, FUNCOP_1:14; hence f " P1 is closed ; ::_thesis: verum end; suppose not y in P1 ; ::_thesis: f " P1 is closed then f " P1 = {} X by A1, FUNCOP_1:16; hence f " P1 is closed ; ::_thesis: verum end; end; end; registration let X be non empty TopSpace; let y be complex number ; clusterX --> y -> continuous ; coherence X --> y is continuous by Th1; end; registration let X be non empty TopSpace; cluster non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() continuous for Element of bool [: the carrier of X,COMPLEX:]; existence ex b1 being Function of the carrier of X,COMPLEX st b1 is continuous proof take f = X --> 0c; ::_thesis: f is continuous thus f is continuous ; ::_thesis: verum end; end; theorem Th2: :: CC0SP2:2 for X being non empty TopSpace for f being Function of the carrier of X,COMPLEX holds ( f is continuous iff for Y being Subset of COMPLEX st Y is open holds f " Y is open ) proof let X be non empty TopSpace; ::_thesis: for f being Function of the carrier of X,COMPLEX holds ( f is continuous iff for Y being Subset of COMPLEX st Y is open holds f " Y is open ) let f be Function of the carrier of X,COMPLEX; ::_thesis: ( f is continuous iff for Y being Subset of COMPLEX st Y is open holds f " Y is open ) hereby ::_thesis: ( ( for Y being Subset of COMPLEX st Y is open holds f " Y is open ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for Y being Subset of COMPLEX st Y is open holds f " Y is open let Y be Subset of COMPLEX; ::_thesis: ( Y is open implies f " Y is open ) assume Y is open ; ::_thesis: f " Y is open then Y ` is closed by CFDIFF_1:def_11; then A2: f " (Y `) is closed by A1, Def1; f " (Y `) = (f " COMPLEX) \ (f " Y) by FUNCT_1:69 .= ([#] X) \ (f " Y) by FUNCT_2:40 ; then ([#] X) \ (([#] X) \ (f " Y)) is open by A2, PRE_TOPC:def_3; hence f " Y is open by PRE_TOPC:3; ::_thesis: verum end; assume A3: for Y being Subset of COMPLEX st Y is open holds f " Y is open ; ::_thesis: f is continuous let Y be Subset of COMPLEX; :: according to CC0SP2:def_1 ::_thesis: ( Y is closed implies f " Y is closed ) assume A4: Y is closed ; ::_thesis: f " Y is closed Y = (Y `) ` ; then Y ` is open by A4, CFDIFF_1:def_11; then A5: f " (Y `) is open by A3; f " (Y `) = (f " COMPLEX) \ (f " Y) by FUNCT_1:69 .= ([#] X) \ (f " Y) by FUNCT_2:40 ; hence f " Y is closed by A5, PRE_TOPC:def_3; ::_thesis: verum end; theorem Th3: :: CC0SP2:3 for X being non empty TopSpace for f being Function of the carrier of X,COMPLEX holds ( f is continuous iff for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ) proof let X be non empty TopSpace; ::_thesis: for f being Function of the carrier of X,COMPLEX holds ( f is continuous iff for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ) let f be Function of the carrier of X,COMPLEX; ::_thesis: ( f is continuous iff for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ) hereby ::_thesis: ( ( for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) now__::_thesis:_for_x_being_Point_of_X for_V_being_Subset_of_COMPLEX_st_f_._x_in_V_&_V_is_open_holds_ ex_W_being_Element_of_bool_the_carrier_of_X_st_ (_x_in_W_&_W_is_open_&_f_.:_W_c=_V_) let x be Point of X; ::_thesis: for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Element of bool the carrier of X st ( x in W & W is open & f .: W c= V ) let V be Subset of COMPLEX; ::_thesis: ( f . x in V & V is open implies ex W being Element of bool the carrier of X st ( x in W & W is open & f .: W c= V ) ) set z = f . x; reconsider z0 = f . x as Complex ; assume ( f . x in V & V is open ) ; ::_thesis: ex W being Element of bool the carrier of X st ( x in W & W is open & f .: W c= V ) then consider N being Neighbourhood of z0 such that A2: N c= V by CFDIFF_1:9; consider g being Real such that A3: ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= N ) by CFDIFF_1:def_5; set S = { y where y is Complex : |.(y - z0).| < g } ; { y where y is Complex : |.(y - z0).| < g } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < g } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z0).| < g } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z0).| < g ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider S1 = { y where y is Complex : |.(y - z0).| < g } as Subset of COMPLEX ; take W = f " { y where y is Complex : |.(y - z0).| < g } ; ::_thesis: ( x in W & W is open & f .: W c= V ) A4: S1 is open by CFDIFF_1:13; { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A3, CFDIFF_1:6; then f . x in { y where y is Complex : |.(y - z0).| < g } by CFDIFF_1:7; hence x in W by FUNCT_2:38; ::_thesis: ( W is open & f .: W c= V ) thus W is open by A1, A4, Th2; ::_thesis: f .: W c= V f .: (f " { y where y is Complex : |.(y - z0).| < g } ) c= { y where y is Complex : |.(y - z0).| < g } by FUNCT_1:75; then f .: W c= N by A3, XBOOLE_1:1; hence f .: W c= V by A2, XBOOLE_1:1; ::_thesis: verum end; hence for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ; ::_thesis: verum end; assume A5: for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ; ::_thesis: f is continuous now__::_thesis:_for_Y_being_Subset_of_COMPLEX_st_Y_is_closed_holds_ f_"_Y_is_closed let Y be Subset of COMPLEX; ::_thesis: ( Y is closed implies f " Y is closed ) assume Y is closed ; ::_thesis: f " Y is closed then (Y `) ` is closed ; then A6: Y ` is open by CFDIFF_1:def_11; for x being Point of X st x in (f " Y) ` holds ex W being Subset of X st ( W is a_neighborhood of x & W c= (f " Y) ` ) proof let x be Point of X; ::_thesis: ( x in (f " Y) ` implies ex W being Subset of X st ( W is a_neighborhood of x & W c= (f " Y) ` ) ) assume x in (f " Y) ` ; ::_thesis: ex W being Subset of X st ( W is a_neighborhood of x & W c= (f " Y) ` ) then x in f " (Y `) by FUNCT_2:100; then f . x in Y ` by FUNCT_2:38; then consider V being Subset of COMPLEX such that A7: ( f . x in V & V is open & V c= Y ` ) by A6; consider W being Subset of X such that A8: ( x in W & W is open & f .: W c= V ) by A5, A7; take W ; ::_thesis: ( W is a_neighborhood of x & W c= (f " Y) ` ) thus W is a_neighborhood of x by A8, CONNSP_2:3; ::_thesis: W c= (f " Y) ` f .: W c= Y ` by A7, A8, XBOOLE_1:1; then A9: f " (f .: W) c= f " (Y `) by RELAT_1:143; W c= f " (f .: W) by FUNCT_2:42; then W c= f " (Y `) by A9, XBOOLE_1:1; hence W c= (f " Y) ` by FUNCT_2:100; ::_thesis: verum end; then (f " Y) ` is open by CONNSP_2:7; then ((f " Y) `) ` is closed by TOPS_1:4; hence f " Y is closed ; ::_thesis: verum end; hence f is continuous by Def1; ::_thesis: verum end; theorem Th4: :: CC0SP2:4 for X being non empty TopSpace for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX proof let X be non empty TopSpace; ::_thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX let f, g be continuous Function of the carrier of X,COMPLEX; ::_thesis: f + g is continuous Function of the carrier of X,COMPLEX set h = f + g; A1: rng (f + g) c= COMPLEX by MEMBERED:1; dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1 .= the carrier of X /\ (dom g) by PARTFUN1:def_2 .= the carrier of X /\ the carrier of X by PARTFUN1:def_2 ; then reconsider h = f + g as Function of the carrier of X,COMPLEX by A1, FUNCT_2:2; A2: for x being Point of X holds h . x = (f . x) + (g . x) by VALUED_1:1; for p being Point of X for V being Subset of COMPLEX st h . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & h .: W c= V ) proof let p be Point of X; ::_thesis: for V being Subset of COMPLEX st h . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & h .: W c= V ) let V be Subset of COMPLEX; ::_thesis: ( h . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & h .: W c= V ) ) assume A3: ( h . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & h .: W c= V ) reconsider z0 = h . p as Complex ; consider N being Neighbourhood of z0 such that A4: N c= V by A3, CFDIFF_1:9; consider r being Real such that A5: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def_5; set S = { y where y is Complex : |.(y - z0).| < r } ; A6: r / 2 is Real by XREAL_0:def_1; reconsider z1 = f . p as Complex ; set S1 = { y where y is Complex : |.(y - z1).| < r / 2 } ; { y where y is Complex : |.(y - z1).| < r / 2 } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / 2 } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z1).| < r / 2 } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z1).| < r / 2 ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / 2 } as Subset of COMPLEX ; A7: T1 is open by A6, CFDIFF_1:13; |.(z1 - z1).| = 0 ; then z1 in { y where y is Complex : |.(y - z1).| < r / 2 } by A5; then consider W1 being Subset of X such that A8: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / 2 } ) by A7, Th3; reconsider z2 = g . p as Complex ; set S2 = { y where y is Complex : |.(y - z2).| < r / 2 } ; { y where y is Complex : |.(y - z2).| < r / 2 } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z2).| < r / 2 } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z2).| < r / 2 } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z2).| < r / 2 ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T2 = { y where y is Complex : |.(y - z2).| < r / 2 } as Subset of COMPLEX ; A9: T2 is open by A6, CFDIFF_1:13; |.(z2 - z2).| = 0 ; then z2 in { y where y is Complex : |.(y - z2).| < r / 2 } by A5; then consider W2 being Subset of X such that A10: ( p in W2 & W2 is open & g .: W2 c= { y where y is Complex : |.(y - z2).| < r / 2 } ) by A9, Th3; set W = W1 /\ W2; A11: W1 /\ W2 is open by A8, A10, TOPS_1:11; A12: p in W1 /\ W2 by A8, A10, XBOOLE_0:def_4; h .: (W1 /\ W2) c= { y where y is Complex : |.(y - z0).| < r } proof let z3 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z3 in h .: (W1 /\ W2) or z3 in { y where y is Complex : |.(y - z0).| < r } ) assume z3 in h .: (W1 /\ W2) ; ::_thesis: z3 in { y where y is Complex : |.(y - z0).| < r } then consider x3 being set such that A13: ( x3 in dom h & x3 in W1 /\ W2 & h . x3 = z3 ) by FUNCT_1:def_6; A14: x3 in W1 by A13, XBOOLE_0:def_4; reconsider px = x3 as Point of X by A13; A15: px in the carrier of X ; then px in dom f by FUNCT_2:def_1; then f . px in f .: W1 by A14, FUNCT_1:def_6; then A16: f . px in { y where y is Complex : |.(y - z1).| < r / 2 } by A8; reconsider a1 = f . px as Complex ; A17: ex aa1 being Complex st ( f . px = aa1 & |.(aa1 - z1).| < r / 2 ) by A16; A18: x3 in W2 by A13, XBOOLE_0:def_4; px in dom g by A15, FUNCT_2:def_1; then g . px in g .: W2 by A18, FUNCT_1:def_6; then A19: g . px in { y where y is Complex : |.(y - z2).| < r / 2 } by A10; reconsider a2 = g . px as Complex ; ex aa2 being Complex st ( g . px = aa2 & |.(aa2 - z2).| < r / 2 ) by A19; then A20: |.(a2 - z2).| < r / 2 ; |.((h . x3) - z0).| = |.(((f . px) + (g . px)) - z0).| by A2 .= |.(((f . px) + (g . px)) - ((f . p) + (g . p))).| by A2 .= |.((a1 - z1) + (a2 - z2)).| ; then A21: |.((h . px) - z0).| <= |.(a1 - z1).| + |.(a2 - z2).| by COMPLEX1:56; A22: |.(a1 - z1).| + |.(a2 - z2).| < (r / 2) + |.(a2 - z2).| by A17, XREAL_1:8; (r / 2) + |.(a2 - z2).| < (r / 2) + (r / 2) by A20, XREAL_1:8; then |.(a1 - z1).| + |.(a2 - z2).| < r by A22, XXREAL_0:2; then |.((h . px) - z0).| < r by A21, XXREAL_0:2; hence z3 in { y where y is Complex : |.(y - z0).| < r } by A13; ::_thesis: verum end; then h .: (W1 /\ W2) c= N by A5, XBOOLE_1:1; hence ex W being Subset of X st ( p in W & W is open & h .: W c= V ) by A11, A12, A4, XBOOLE_1:1; ::_thesis: verum end; hence f + g is continuous Function of the carrier of X,COMPLEX by Th3; ::_thesis: verum end; theorem Th5: :: CC0SP2:5 for X being non empty TopSpace for a being complex number for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX proof let X be non empty TopSpace; ::_thesis: for a being complex number for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX let a be complex number ; ::_thesis: for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX let f be continuous Function of the carrier of X,COMPLEX; ::_thesis: a (#) f is continuous Function of the carrier of X,COMPLEX set h = a (#) f; A1: for x being Point of X holds (a (#) f) . x = a * (f . x) by VALUED_1:6; now__::_thesis:_a_(#)_f_is_continuous percases ( a <> 0 or a = 0 ) ; supposeA2: a <> 0 ; ::_thesis: a (#) f is continuous for p being Point of X for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & (a (#) f) .: W c= V ) proof let p be Point of X; ::_thesis: for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & (a (#) f) .: W c= V ) let V be Subset of COMPLEX; ::_thesis: ( (a (#) f) . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & (a (#) f) .: W c= V ) ) assume A3: ( (a (#) f) . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & (a (#) f) .: W c= V ) reconsider z0 = (a (#) f) . p as Complex ; consider N being Neighbourhood of z0 such that A4: N c= V by A3, CFDIFF_1:9; consider r being Real such that A5: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def_5; set S = { y where y is Complex : |.(y - z0).| < r } ; A6: |.a.| > 0 by A2; A7: r / |.a.| is Real by XREAL_0:def_1; A8: r / |.a.| > 0 by A2, A5; reconsider z1 = f . p as Complex ; set S1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } ; { y where y is Complex : |.(y - z1).| < r / |.a.| } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / |.a.| } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z1).| < r / |.a.| } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z1).| < r / |.a.| ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } as Subset of COMPLEX ; A9: T1 is open by A7, CFDIFF_1:13; |.(z1 - z1).| = 0 ; then z1 in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A8; then consider W1 being Subset of X such that A10: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / |.a.| } ) by A9, Th3; set W = W1; A11: W1 is open by A10; A12: p in W1 by A10; (a (#) f) .: W1 c= { y where y is Complex : |.(y - z0).| < r } proof let z3 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z3 in (a (#) f) .: W1 or z3 in { y where y is Complex : |.(y - z0).| < r } ) assume z3 in (a (#) f) .: W1 ; ::_thesis: z3 in { y where y is Complex : |.(y - z0).| < r } then consider x3 being set such that A13: ( x3 in dom (a (#) f) & x3 in W1 & (a (#) f) . x3 = z3 ) by FUNCT_1:def_6; reconsider px = x3 as Point of X by A13; px in the carrier of X ; then px in dom f by FUNCT_2:def_1; then f . px in f .: W1 by A13, FUNCT_1:def_6; then A14: f . px in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A10; reconsider a1 = f . px as Complex ; ex aa1 being Complex st ( f . px = aa1 & |.(aa1 - z1).| < r / |.a.| ) by A14; then A15: |.(a1 - z1).| < r / |.a.| ; A16: |.(((a (#) f) . x3) - z0).| = |.((a * (f . px)) - z0).| by A1 .= |.((a * (f . px)) - (a * (f . p))).| by A1 .= |.(a * ((f . px) - (f . p))).| .= |.a.| * |.(a1 - z1).| by COMPLEX1:65 ; A17: |.a.| * |.(a1 - z1).| < |.a.| * (r / |.a.|) by A6, A15, XREAL_1:68; |.a.| * (r / |.a.|) = r * (|.a.| / |.a.|) .= r * 1 by A6, XCMPLX_1:60 .= r ; then |.(((a (#) f) . px) - z0).| < r by A16, A17; hence z3 in { y where y is Complex : |.(y - z0).| < r } by A13; ::_thesis: verum end; then (a (#) f) .: W1 c= N by A5, XBOOLE_1:1; hence ex W being Subset of X st ( p in W & W is open & (a (#) f) .: W c= V ) by A11, A12, A4, XBOOLE_1:1; ::_thesis: verum end; hence a (#) f is continuous by Th3; ::_thesis: verum end; supposeA18: a = 0 ; ::_thesis: a (#) f is continuous set g = X --> 0c; set CX = the carrier of X; A19: dom (X --> 0c) = the carrier of X by FUNCOP_1:13; dom (a (#) f) = the carrier of X by FUNCT_2:def_1; then A20: dom (X --> 0c) = dom (a (#) f) by A19; for z being set st z in dom (a (#) f) holds (X --> 0c) . z = (a (#) f) . z proof let z be set ; ::_thesis: ( z in dom (a (#) f) implies (X --> 0c) . z = (a (#) f) . z ) assume A21: z in dom (a (#) f) ; ::_thesis: (X --> 0c) . z = (a (#) f) . z (a (#) f) . z = 0 * (f . z) by A18, VALUED_1:6 .= 0 ; hence (X --> 0c) . z = (a (#) f) . z by A21, FUNCOP_1:7; ::_thesis: verum end; hence a (#) f is continuous by A20, FUNCT_1:def_11; ::_thesis: verum end; end; end; hence a (#) f is continuous Function of the carrier of X,COMPLEX ; ::_thesis: verum end; theorem :: CC0SP2:6 for X being non empty TopSpace for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX proof let X be non empty TopSpace; ::_thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX let f, g be continuous Function of the carrier of X,COMPLEX; ::_thesis: f - g is continuous Function of the carrier of X,COMPLEX (- 1) (#) g is continuous by Th5; hence f - g is continuous Function of the carrier of X,COMPLEX by Th4; ::_thesis: verum end; theorem Th7: :: CC0SP2:7 for X being non empty TopSpace for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX proof let X be non empty TopSpace; ::_thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX let f, g be continuous Function of the carrier of X,COMPLEX; ::_thesis: f (#) g is continuous Function of the carrier of X,COMPLEX set h = f (#) g; A1: for x being Point of X holds (f (#) g) . x = (f . x) * (g . x) by VALUED_1:5; for p being Point of X for V being Subset of COMPLEX st (f (#) g) . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & (f (#) g) .: W c= V ) proof let p be Point of X; ::_thesis: for V being Subset of COMPLEX st (f (#) g) . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & (f (#) g) .: W c= V ) let V be Subset of COMPLEX; ::_thesis: ( (f (#) g) . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & (f (#) g) .: W c= V ) ) assume A2: ( (f (#) g) . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & (f (#) g) .: W c= V ) reconsider z0 = (f (#) g) . p as Complex ; consider N being Neighbourhood of z0 such that A3: N c= V by A2, CFDIFF_1:9; consider r being Real such that A4: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def_5; set S = { y where y is Complex : |.(y - z0).| < r } ; reconsider z1 = f . p as Complex ; reconsider z2 = g . p as Complex ; set a = (|.z1.| + |.z2.|) + 1; A5: r / ((|.z1.| + |.z2.|) + 1) is Real by XREAL_0:def_1; set S1 = { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ; { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } as Subset of COMPLEX ; A6: T1 is open by A5, CFDIFF_1:13; |.(z1 - z1).| = 0 ; then z1 in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } by A4; then consider W1 being Subset of X such that A7: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ) by A6, Th3; set S2 = { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ; { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T2 = { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } as Subset of COMPLEX ; A8: T2 is open by A5, CFDIFF_1:13; |.(z2 - z2).| = 0 ; then z2 in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } by A4; then consider W2 being Subset of X such that A9: ( p in W2 & W2 is open & g .: W2 c= { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ) by A8, Th3; set S3 = { y where y is Complex : |.(y - z1).| < 1 } ; { y where y is Complex : |.(y - z1).| < 1 } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < 1 } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z1).| < 1 } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z1).| < 1 ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T3 = { y where y is Complex : |.(y - z1).| < 1 } as Subset of COMPLEX ; A10: T3 is open by CFDIFF_1:13; |.(z1 - z1).| = 0 ; then z1 in { y where y is Complex : |.(y - z1).| < 1 } ; then consider W3 being Subset of X such that A11: ( p in W3 & W3 is open & f .: W3 c= { y where y is Complex : |.(y - z1).| < 1 } ) by A10, Th3; set W = (W1 /\ W2) /\ W3; W1 /\ W2 is open by A7, A9, TOPS_1:11; then A12: (W1 /\ W2) /\ W3 is open by A11, TOPS_1:11; p in W1 /\ W2 by A7, A9, XBOOLE_0:def_4; then A13: p in (W1 /\ W2) /\ W3 by A11, XBOOLE_0:def_4; (f (#) g) .: ((W1 /\ W2) /\ W3) c= { y where y is Complex : |.(y - z0).| < r } proof let z3 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z3 in (f (#) g) .: ((W1 /\ W2) /\ W3) or z3 in { y where y is Complex : |.(y - z0).| < r } ) assume z3 in (f (#) g) .: ((W1 /\ W2) /\ W3) ; ::_thesis: z3 in { y where y is Complex : |.(y - z0).| < r } then consider x3 being set such that A14: ( x3 in dom (f (#) g) & x3 in (W1 /\ W2) /\ W3 & (f (#) g) . x3 = z3 ) by FUNCT_1:def_6; A15: x3 in W1 /\ W2 by A14, XBOOLE_0:def_4; then A16: x3 in W1 by XBOOLE_0:def_4; reconsider px = x3 as Point of X by A14; A17: px in the carrier of X ; then px in dom f by FUNCT_2:def_1; then f . px in f .: W1 by A16, FUNCT_1:def_6; then A18: f . px in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } by A7; reconsider a1 = f . px as Complex ; ex aa1 being Complex st ( f . px = aa1 & |.(aa1 - z1).| < r / ((|.z1.| + |.z2.|) + 1) ) by A18; then A19: |.(a1 - z1).| < r / ((|.z1.| + |.z2.|) + 1) ; A20: x3 in W2 by A15, XBOOLE_0:def_4; px in dom g by A17, FUNCT_2:def_1; then g . px in g .: W2 by A20, FUNCT_1:def_6; then A21: g . px in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } by A9; reconsider a2 = g . px as Complex ; ex aa2 being Complex st ( g . px = aa2 & |.(aa2 - z2).| < r / ((|.z1.| + |.z2.|) + 1) ) by A21; then A22: |.(a2 - z2).| < r / ((|.z1.| + |.z2.|) + 1) ; A23: x3 in W3 by A14, XBOOLE_0:def_4; px in dom f by A17, FUNCT_2:def_1; then f . px in f .: W3 by A23, FUNCT_1:def_6; then A24: f . px in { y where y is Complex : |.(y - z1).| < 1 } by A11; reconsider a3 = f . px as Complex ; ex aa3 being Complex st ( f . px = aa3 & |.(aa3 - z1).| < 1 ) by A24; then A25: |.(a3 - z1).| < 1 ; |.((a1 - z1) + z1).| <= |.(a1 - z1).| + |.z1.| by COMPLEX1:56; then |.a1.| - |.z1.| <= (|.(a1 - z1).| + |.z1.|) - |.z1.| by XREAL_1:9; then |.a1.| - |.z1.| < 1 by A25, XXREAL_0:2; then (|.a1.| - |.z1.|) + |.z1.| < 1 + |.z1.| by XREAL_1:8; then A26: |.a1.| < 1 + |.z1.| ; A27: |.(((f (#) g) . x3) - z0).| = |.(((f . px) * (g . px)) - z0).| by A1 .= |.((a1 * a2) - (z1 * z2)).| by A1 .= |.(((a1 * a2) - (a1 * z2)) + ((a1 * z2) - (z1 * z2))).| ; A28: |.(((f (#) g) . x3) - z0).| <= |.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).| by A27, COMPLEX1:56; |.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).| = |.(a1 * (a2 - z2)).| + |.(z2 * (a1 - z1)).| .= (|.a1.| * |.(a2 - z2).|) + |.(z2 * (a1 - z1)).| by COMPLEX1:65 .= (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) by COMPLEX1:65 ; then A29: |.(((f (#) g) . x3) - z0).| <= (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) by A28; A30: |.a1.| * |.(a2 - z2).| <= |.a1.| * (r / ((|.z1.| + |.z2.|) + 1)) by A22, XREAL_1:66; |.a1.| * (r / ((|.z1.| + |.z2.|) + 1)) < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1)) by A26, A4, XREAL_1:68; then A31: |.a1.| * |.(a2 - z2).| < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1)) by A30, XXREAL_0:2; A32: |.z2.| * |.(a1 - z1).| <= |.z2.| * (r / ((|.z1.| + |.z2.|) + 1)) by A19, XREAL_1:66; A33: (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|) by A31, XREAL_1:8; ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|) <= ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1))) by A32, XREAL_1:6; then (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1))) by A33, XXREAL_0:2; then A34: |.(((f (#) g) . x3) - z0).| < r * (((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1)) by A29, XXREAL_0:2; ((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1) = 1 by XCMPLX_0:def_7; then |.(((f (#) g) . px) - z0).| < r by A34; hence z3 in { y where y is Complex : |.(y - z0).| < r } by A14; ::_thesis: verum end; then (f (#) g) .: ((W1 /\ W2) /\ W3) c= N by A4, XBOOLE_1:1; hence ex W being Subset of X st ( p in W & W is open & (f (#) g) .: W c= V ) by A12, A13, A3, XBOOLE_1:1; ::_thesis: verum end; hence f (#) g is continuous Function of the carrier of X,COMPLEX by Th3; ::_thesis: verum end; theorem Th8: :: CC0SP2:8 for X being non empty TopSpace for f being continuous Function of the carrier of X,COMPLEX holds ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) proof let X be non empty TopSpace; ::_thesis: for f being continuous Function of the carrier of X,COMPLEX holds ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) let f be continuous Function of the carrier of X,COMPLEX; ::_thesis: ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) reconsider h = |.f.| as Function of the carrier of X,REAL ; for p being Point of X for V being Subset of REAL st h . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & h .: W c= V ) proof let p be Point of X; ::_thesis: for V being Subset of REAL st h . p in V & V is open holds ex W being Subset of X st ( p in W & W is open & h .: W c= V ) let V be Subset of REAL; ::_thesis: ( h . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & h .: W c= V ) ) assume A1: ( h . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & h .: W c= V ) reconsider r0 = h . p as Real ; consider r being real number such that A2: ( 0 < r & ].(r0 - r),(r0 + r).[ c= V ) by A1, RCOMP_1:19; set S = ].(r0 - r),(r0 + r).[; reconsider z1 = f . p as Complex ; set S1 = { y where y is Complex : |.(y - z1).| < r } ; { y where y is Complex : |.(y - z1).| < r } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r } or z in COMPLEX ) assume z in { y where y is Complex : |.(y - z1).| < r } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - z1).| < r ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T1 = { y where y is Complex : |.(y - z1).| < r } as Subset of COMPLEX ; r is Real by XREAL_0:def_1; then A3: T1 is open by CFDIFF_1:13; |.(z1 - z1).| = 0 ; then z1 in { y where y is Complex : |.(y - z1).| < r } by A2; then consider W1 being Subset of X such that A4: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r } ) by A3, Th3; set W = W1; A5: W1 is open by A4; A6: p in W1 by A4; h .: W1 c= ].(r0 - r),(r0 + r).[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h .: W1 or x in ].(r0 - r),(r0 + r).[ ) assume x in h .: W1 ; ::_thesis: x in ].(r0 - r),(r0 + r).[ then consider z being set such that A7: ( z in dom h & z in W1 & h . z = x ) by FUNCT_1:def_6; A8: z in W1 by A7; reconsider pz = z as Point of X by A7; pz in the carrier of X ; then pz in dom f by FUNCT_2:def_1; then f . pz in f .: W1 by A8, FUNCT_1:def_6; then A9: f . pz in { y where y is Complex : |.(y - z1).| < r } by A4; reconsider a1 = f . pz as Complex ; ex aa1 being Complex st ( f . pz = aa1 & |.(aa1 - z1).| < r ) by A9; then A10: |.(a1 - z1).| < r ; A11: |.((h . z) - r0).| = |.(|.(f . pz).| - (|.f.| . p)).| by VALUED_1:18 .= |.(|.(f . pz).| - |.(f . p).|).| by VALUED_1:18 ; |.(|.(f . pz).| - |.(f . p).|).| <= |.((f . pz) - (f . p)).| by COMPLEX1:64; then |.(|.(f . pz).| - |.(f . p).|).| < r by A10, XXREAL_0:2; hence x in ].(r0 - r),(r0 + r).[ by A7, A11, RCOMP_1:1; ::_thesis: verum end; hence ex W being Subset of X st ( p in W & W is open & h .: W c= V ) by A5, A6, A2, XBOOLE_1:1; ::_thesis: verum end; hence ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) by C0SP2:1; ::_thesis: verum end; definition let X be non empty TopSpace; func CContinuousFunctions X -> Subset of (CAlgebra the carrier of X) equals :: CC0SP2:def 3 { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; correctness coherence { f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X); proof set A = { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; { f where f is continuous Function of the carrier of X,COMPLEX : verum } c= Funcs ( the carrier of X,COMPLEX) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is continuous Function of the carrier of X,COMPLEX : verum } or x in Funcs ( the carrier of X,COMPLEX) ) assume x in { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; ::_thesis: x in Funcs ( the carrier of X,COMPLEX) then ex f being continuous Function of the carrier of X,COMPLEX st x = f ; hence x in Funcs ( the carrier of X,COMPLEX) by FUNCT_2:8; ::_thesis: verum end; hence { f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X) ; ::_thesis: verum end; end; :: deftheorem defines CContinuousFunctions CC0SP2:def_3_:_ for X being non empty TopSpace holds CContinuousFunctions X = { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; registration let X be non empty TopSpace; cluster CContinuousFunctions X -> non empty ; coherence not CContinuousFunctions X is empty proof X --> 0c in { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; hence not CContinuousFunctions X is empty ; ::_thesis: verum end; end; registration let X be non empty TopSpace; cluster CContinuousFunctions X -> multiplicatively-closed Cadditively-linearly-closed ; coherence ( CContinuousFunctions X is Cadditively-linearly-closed & CContinuousFunctions X is multiplicatively-closed ) proof set W = CContinuousFunctions X; set V = CAlgebra the carrier of X; for v, u being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X & u in CContinuousFunctions X holds v + u in CContinuousFunctions X proof let v, u be Element of (CAlgebra the carrier of X); ::_thesis: ( v in CContinuousFunctions X & u in CContinuousFunctions X implies v + u in CContinuousFunctions X ) assume A1: ( v in CContinuousFunctions X & u in CContinuousFunctions X ) ; ::_thesis: v + u in CContinuousFunctions X consider v1 being continuous Function of the carrier of X,COMPLEX such that A2: v1 = v by A1; consider u1 being continuous Function of the carrier of X,COMPLEX such that A3: u1 = u by A1; reconsider h = v + u as Element of Funcs ( the carrier of X,COMPLEX) ; A4: ex f being Function st ( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2; (dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1; then A5: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def_1; for x being set st x in dom h holds h . x = (v1 . x) + (u1 . x) by A2, A3, CFUNCDOM:1; then A6: v + u = v1 + u1 by A5, A4, VALUED_1:def_1; v1 + u1 is continuous Function of the carrier of X,COMPLEX by Th4; hence v + u in CContinuousFunctions X by A6; ::_thesis: verum end; then A7: CContinuousFunctions X is add-closed by IDEAL_1:def_1; for v being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X holds - v in CContinuousFunctions X proof let v be Element of (CAlgebra the carrier of X); ::_thesis: ( v in CContinuousFunctions X implies - v in CContinuousFunctions X ) assume A8: v in CContinuousFunctions X ; ::_thesis: - v in CContinuousFunctions X consider v1 being continuous Function of the carrier of X,COMPLEX such that A9: v1 = v by A8; reconsider h = - v, v2 = v as Element of Funcs ( the carrier of X,COMPLEX) ; reconsider e = - 1r as Complex ; A10: h = e * v by CLVECT_1:3; A11: ex f being Function st ( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2; A12: dom v1 = the carrier of X by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_ h_._x_=_-_(v1_._x) let x be set ; ::_thesis: ( x in dom h implies h . x = - (v1 . x) ) assume x in dom h ; ::_thesis: h . x = - (v1 . x) then reconsider y = x as Element of the carrier of X ; h . x = (- 1) * (v2 . y) by A10, CFUNCDOM:4; hence h . x = - (v1 . x) by A9; ::_thesis: verum end; then A13: - v = - v1 by A12, A11, VALUED_1:9; e (#) v1 is continuous Function of the carrier of X,COMPLEX by Th5; hence - v in CContinuousFunctions X by A13; ::_thesis: verum end; then A14: CContinuousFunctions X is having-inverse by C0SP1:def_1; for a being Complex for u being Element of (CAlgebra the carrier of X) st u in CContinuousFunctions X holds a * u in CContinuousFunctions X proof let a be Complex; ::_thesis: for u being Element of (CAlgebra the carrier of X) st u in CContinuousFunctions X holds a * u in CContinuousFunctions X let u be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CContinuousFunctions X implies a * u in CContinuousFunctions X ) assume A15: u in CContinuousFunctions X ; ::_thesis: a * u in CContinuousFunctions X consider u1 being continuous Function of the carrier of X,COMPLEX such that A16: u1 = u by A15; reconsider h = a * u as Element of Funcs ( the carrier of X,COMPLEX) ; A17: ex f being Function st ( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2; A18: dom u1 = the carrier of X by FUNCT_2:def_1; a in COMPLEX by XCMPLX_0:def_2; then for x being set st x in dom h holds h . x = a * (u1 . x) by A16, CFUNCDOM:4; then A19: a * u = a (#) u1 by A18, A17, VALUED_1:def_5; a (#) u1 is continuous Function of the carrier of X,COMPLEX by Th5; hence a * u in CContinuousFunctions X by A19; ::_thesis: verum end; hence CContinuousFunctions X is Cadditively-linearly-closed by A7, A14, CC0SP1:def_2; ::_thesis: CContinuousFunctions X is multiplicatively-closed A20: for v, u being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X & u in CContinuousFunctions X holds v * u in CContinuousFunctions X proof let v, u be Element of (CAlgebra the carrier of X); ::_thesis: ( v in CContinuousFunctions X & u in CContinuousFunctions X implies v * u in CContinuousFunctions X ) assume A21: ( v in CContinuousFunctions X & u in CContinuousFunctions X ) ; ::_thesis: v * u in CContinuousFunctions X consider v1 being continuous Function of the carrier of X,COMPLEX such that A22: v1 = v by A21; consider u1 being continuous Function of the carrier of X,COMPLEX such that A23: u1 = u by A21; reconsider h = v * u as Element of Funcs ( the carrier of X,COMPLEX) ; A24: ex f being Function st ( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2; (dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1; then A25: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def_1; for x being set st x in dom h holds h . x = (v1 . x) * (u1 . x) by A22, A23, CFUNCDOM:2; then A26: v * u = v1 (#) u1 by A25, A24, VALUED_1:def_4; v1 (#) u1 is continuous Function of the carrier of X,COMPLEX by Th7; hence v * u in CContinuousFunctions X by A26; ::_thesis: verum end; reconsider g = ComplexFuncUnit the carrier of X as Function of the carrier of X,COMPLEX ; g = X --> 1r ; then 1. (CAlgebra the carrier of X) in CContinuousFunctions X ; hence CContinuousFunctions X is multiplicatively-closed by A20, C0SP1:def_4; ::_thesis: verum end; end; definition let X be non empty TopSpace; func C_Algebra_of_ContinuousFunctions X -> ComplexAlgebra equals :: CC0SP2:def 4 ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #); coherence ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #) is ComplexAlgebra by CC0SP1:2; end; :: deftheorem defines C_Algebra_of_ContinuousFunctions CC0SP2:def_4_:_ for X being non empty TopSpace holds C_Algebra_of_ContinuousFunctions X = ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #); theorem :: CC0SP2:9 for X being non empty TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; registration let X be non empty TopSpace; cluster C_Algebra_of_ContinuousFunctions X -> strict ; coherence ( C_Algebra_of_ContinuousFunctions X is strict & not C_Algebra_of_ContinuousFunctions X is empty ) ; end; registration let X be non empty TopSpace; cluster C_Algebra_of_ContinuousFunctions X -> scalar-unital ; coherence ( C_Algebra_of_ContinuousFunctions X is Abelian & C_Algebra_of_ContinuousFunctions X is add-associative & C_Algebra_of_ContinuousFunctions X is right_zeroed & C_Algebra_of_ContinuousFunctions X is right_complementable & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is scalar-unital & C_Algebra_of_ContinuousFunctions X is commutative & C_Algebra_of_ContinuousFunctions X is associative & C_Algebra_of_ContinuousFunctions X is right_unital & C_Algebra_of_ContinuousFunctions X is right-distributive & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is vector-associative ) proof now__::_thesis:_for_v_being_VECTOR_of_(C_Algebra_of_ContinuousFunctions_X)_holds_1r_*_v_=_v let v be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: 1r * v = v reconsider v1 = v as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3; C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; then 1r * v = 1r * v1 by CC0SP1:3; hence 1r * v = v by CFUNCDOM:12; ::_thesis: verum end; hence ( C_Algebra_of_ContinuousFunctions X is Abelian & C_Algebra_of_ContinuousFunctions X is add-associative & C_Algebra_of_ContinuousFunctions X is right_zeroed & C_Algebra_of_ContinuousFunctions X is right_complementable & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is scalar-unital & C_Algebra_of_ContinuousFunctions X is commutative & C_Algebra_of_ContinuousFunctions X is associative & C_Algebra_of_ContinuousFunctions X is right_unital & C_Algebra_of_ContinuousFunctions X is right-distributive & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is vector-associative ) by CLVECT_1:def_5; ::_thesis: verum end; end; theorem Th10: :: CC0SP2:10 for X being non empty TopSpace for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) proof let X be non empty TopSpace; ::_thesis: for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) let F, G, H be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) ) assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; reconsider f1 = F, g1 = G, h1 = H as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3; hereby ::_thesis: ( ( for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) implies H = F + G ) assume A3: H = F + G ; ::_thesis: for x being Element of the carrier of X holds h . x = (f . x) + (g . x) let x be Element of the carrier of X; ::_thesis: h . x = (f . x) + (g . x) h1 = f1 + g1 by A2, A3, CC0SP1:3; hence h . x = (f . x) + (g . x) by A1, CFUNCDOM:1; ::_thesis: verum end; assume for x being Element of X holds h . x = (f . x) + (g . x) ; ::_thesis: H = F + G then h1 = f1 + g1 by A1, CFUNCDOM:1; hence H = F + G by A2, CC0SP1:3; ::_thesis: verum end; theorem Th11: :: CC0SP2:11 for X being non empty TopSpace for F, G being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g being Function of the carrier of X,COMPLEX for a being Complex st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) proof let X be non empty TopSpace; ::_thesis: for F, G being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g being Function of the carrier of X,COMPLEX for a being Complex st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) let F, G be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g being Function of the carrier of X,COMPLEX for a being Complex st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) let f, g be Function of the carrier of X,COMPLEX; ::_thesis: for a being Complex st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) let a be Complex; ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) ) assume A1: ( f = F & g = G ) ; ::_thesis: ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; reconsider f1 = F, g1 = G as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3; A3: a in COMPLEX by XCMPLX_0:def_2; hereby ::_thesis: ( ( for x being Element of X holds g . x = a * (f . x) ) implies G = a * F ) assume A4: G = a * F ; ::_thesis: for x being Element of the carrier of X holds g . x = a * (f . x) let x be Element of the carrier of X; ::_thesis: g . x = a * (f . x) g1 = a * f1 by A2, A4, CC0SP1:3; hence g . x = a * (f . x) by A1, A3, CFUNCDOM:4; ::_thesis: verum end; assume for x being Element of the carrier of X holds g . x = a * (f . x) ; ::_thesis: G = a * F then g1 = a * f1 by A1, A3, CFUNCDOM:4; hence G = a * F by A2, CC0SP1:3; ::_thesis: verum end; theorem Th12: :: CC0SP2:12 for X being non empty TopSpace for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) proof let X be non empty TopSpace; ::_thesis: for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) let F, G, H be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) ) assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; reconsider f1 = F, g1 = G, h1 = H as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3; hereby ::_thesis: ( ( for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) implies H = F * G ) assume A3: H = F * G ; ::_thesis: for x being Element of the carrier of X holds h . x = (f . x) * (g . x) let x be Element of the carrier of X; ::_thesis: h . x = (f . x) * (g . x) h1 = f1 * g1 by A2, A3, CC0SP1:3; hence h . x = (f . x) * (g . x) by A1, CFUNCDOM:2; ::_thesis: verum end; assume for x being Element of X holds h . x = (f . x) * (g . x) ; ::_thesis: H = F * G then h1 = f1 * g1 by A1, CFUNCDOM:2; hence H = F * G by A2, CC0SP1:3; ::_thesis: verum end; theorem Th13: :: CC0SP2:13 for X being non empty TopSpace holds 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0c proof let X be non empty TopSpace; ::_thesis: 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0c A1: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; 0. (CAlgebra the carrier of X) = X --> 0c ; hence 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0 by A1, CC0SP1:3; ::_thesis: verum end; theorem Th14: :: CC0SP2:14 for X being non empty TopSpace holds 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r proof let X be non empty TopSpace; ::_thesis: 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r A1: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; 1_ (CAlgebra the carrier of X) = X --> 1r ; hence 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r by A1, CC0SP1:3; ::_thesis: verum end; theorem Th15: :: CC0SP2:15 for A being ComplexAlgebra for A1, A2 being ComplexSubAlgebra of A st the carrier of A1 c= the carrier of A2 holds A1 is ComplexSubAlgebra of A2 proof let A be ComplexAlgebra; ::_thesis: for A1, A2 being ComplexSubAlgebra of A st the carrier of A1 c= the carrier of A2 holds A1 is ComplexSubAlgebra of A2 let A1, A2 be ComplexSubAlgebra of A; ::_thesis: ( the carrier of A1 c= the carrier of A2 implies A1 is ComplexSubAlgebra of A2 ) assume A1: the carrier of A1 c= the carrier of A2 ; ::_thesis: A1 is ComplexSubAlgebra of A2 set CA1 = the carrier of A1; set CA2 = the carrier of A2; set AA = the addF of A; set mA = the multF of A; set MA = the Mult of A; A2: ( 0. A1 = 0. A & 0. A2 = 0. A & 1. A1 = 1. A & 1. A2 = 1. A ) by CC0SP1:def_1; A3: the addF of A1 = the addF of A2 || the carrier of A1 proof ( the addF of A1 = the addF of A || the carrier of A1 & the addF of A2 = the addF of A || the carrier of A2 & [: the carrier of A1, the carrier of A1:] c= [: the carrier of A2, the carrier of A2:] ) by A1, CC0SP1:def_1, ZFMISC_1:96; hence the addF of A1 = the addF of A2 || the carrier of A1 by FUNCT_1:51; ::_thesis: verum end; A4: the multF of A1 = the multF of A2 || the carrier of A1 proof ( the multF of A1 = the multF of A || the carrier of A1 & the multF of A2 = the multF of A || the carrier of A2 & [: the carrier of A1, the carrier of A1:] c= [: the carrier of A2, the carrier of A2:] ) by A1, CC0SP1:def_1, ZFMISC_1:96; hence the multF of A1 = the multF of A2 || the carrier of A1 by FUNCT_1:51; ::_thesis: verum end; the Mult of A1 = the Mult of A2 | [:COMPLEX, the carrier of A1:] proof ( the Mult of A1 = the Mult of A | [:COMPLEX, the carrier of A1:] & the Mult of A2 = the Mult of A | [:COMPLEX, the carrier of A2:] & [:COMPLEX, the carrier of A1:] c= [:COMPLEX, the carrier of A2:] ) by A1, CC0SP1:def_1, ZFMISC_1:96; hence the Mult of A1 = the Mult of A2 | [:COMPLEX, the carrier of A1:] by FUNCT_1:51; ::_thesis: verum end; hence A1 is ComplexSubAlgebra of A2 by A1, A2, A3, A4, CC0SP1:def_1; ::_thesis: verum end; Lm1: for X being non empty compact TopSpace for x being set st x in CContinuousFunctions X holds x in ComplexBoundedFunctions the carrier of X proof let X be non empty compact TopSpace; ::_thesis: for x being set st x in CContinuousFunctions X holds x in ComplexBoundedFunctions the carrier of X let x be set ; ::_thesis: ( x in CContinuousFunctions X implies x in ComplexBoundedFunctions the carrier of X ) assume x in CContinuousFunctions X ; ::_thesis: x in ComplexBoundedFunctions the carrier of X then consider h being continuous Function of the carrier of X,COMPLEX such that A1: x = h ; ( |.h.| is Function of the carrier of X,REAL & |.h.| is continuous ) by Th8; then consider h1 being Function of the carrier of X,REAL such that A2: ( h1 = |.h.| & h1 is continuous ) ; ( h1 is bounded_above & h1 is bounded_below ) by A2, SEQ_2:def_8; then consider r1 being real number such that A3: for y being set st y in dom h1 holds h1 . y < r1 by SEQ_2:def_1; A4: for y being set st y in dom h holds abs (h . y) < r1 proof let y be set ; ::_thesis: ( y in dom h implies abs (h . y) < r1 ) assume A5: y in dom h ; ::_thesis: abs (h . y) < r1 A6: dom h1 = dom h by A2, VALUED_1:def_11; h1 . y = |.(h . y).| by A2, VALUED_1:18 .= abs (h . y) ; hence abs (h . y) < r1 by A3, A5, A6; ::_thesis: verum end; h is bounded by A4, COMSEQ_2:def_3; then h | the carrier of X is bounded by FUNCT_2:33; hence x in ComplexBoundedFunctions the carrier of X by A1; ::_thesis: verum end; theorem :: CC0SP2:16 for X being non empty compact TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X proof let X be non empty compact TopSpace; ::_thesis: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X A1: the carrier of (C_Algebra_of_ContinuousFunctions X) c= the carrier of (C_Algebra_of_BoundedFunctions the carrier of X) proof for x being set st x in CContinuousFunctions X holds x in ComplexBoundedFunctions the carrier of X by Lm1; hence the carrier of (C_Algebra_of_ContinuousFunctions X) c= the carrier of (C_Algebra_of_BoundedFunctions the carrier of X) by TARSKI:def_3; ::_thesis: verum end; A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2; C_Algebra_of_BoundedFunctions the carrier of X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:4; hence C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X by A1, A2, Th15; ::_thesis: verum end; definition let X be non empty compact TopSpace; func CContinuousFunctionsNorm X -> Function of (CContinuousFunctions X),REAL equals :: CC0SP2:def 5 (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X); correctness coherence (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL; proof for x being set st x in CContinuousFunctions X holds x in ComplexBoundedFunctions the carrier of X by Lm1; then CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X by TARSKI:def_3; hence (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL by FUNCT_2:32; ::_thesis: verum end; end; :: deftheorem defines CContinuousFunctionsNorm CC0SP2:def_5_:_ for X being non empty compact TopSpace holds CContinuousFunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X); definition let X be non empty compact TopSpace; func C_Normed_Algebra_of_ContinuousFunctions X -> Normed_Complex_AlgebraStr equals :: CC0SP2:def 6 Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #); correctness coherence Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #) is Normed_Complex_AlgebraStr ; ; end; :: deftheorem defines C_Normed_Algebra_of_ContinuousFunctions CC0SP2:def_6_:_ for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X = Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #); registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> non empty strict ; correctness coherence ( not C_Normed_Algebra_of_ContinuousFunctions X is empty & C_Normed_Algebra_of_ContinuousFunctions X is strict ); ; end; Lm2: now__::_thesis:_for_X_being_non_empty_compact_TopSpace for_x,_e_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_st_e_=_One__((CContinuousFunctions_X),(CAlgebra_the_carrier_of_X))_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let X be non empty compact TopSpace; ::_thesis: for x, e being Element of (C_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) holds ( x * e = x & e * x = x ) set F = C_Normed_Algebra_of_ContinuousFunctions X; let x, e be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) ) assume A1: e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) ; ::_thesis: ( x * e = x & e * x = x ) set X1 = CContinuousFunctions X; reconsider f = x as Element of CContinuousFunctions X ; 1_ (CAlgebra the carrier of X) = X --> 1 .= 1_ (C_Algebra_of_ContinuousFunctions X) by Th14 ; then A2: ( [f,(1_ (CAlgebra the carrier of X))] in [:(CContinuousFunctions X),(CContinuousFunctions X):] & [(1_ (CAlgebra the carrier of X)),f] in [:(CContinuousFunctions X),(CContinuousFunctions X):] ) by ZFMISC_1:87; x * e = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (f,(1_ (CAlgebra the carrier of X))) by A1, C0SP1:def_8; then x * e = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . (f,(1_ (CAlgebra the carrier of X))) by C0SP1:def_6; then x * e = f * (1_ (CAlgebra the carrier of X)) by A2, FUNCT_1:49; hence x * e = x by VECTSP_1:def_4; ::_thesis: e * x = x e * x = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . ((1_ (CAlgebra the carrier of X)),f) by A1, C0SP1:def_8; then e * x = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . ((1_ (CAlgebra the carrier of X)),f) by C0SP1:def_6; then e * x = (1_ (CAlgebra the carrier of X)) * f by A2, FUNCT_1:49; hence e * x = x by VECTSP_1:def_4; ::_thesis: verum end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> unital ; correctness coherence C_Normed_Algebra_of_ContinuousFunctions X is unital ; proof reconsider e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) as Element of (C_Normed_Algebra_of_ContinuousFunctions X) ; take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions X) holds ( b1 * e = b1 & e * b1 = b1 ) thus for b1 being Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions X) holds ( b1 * e = b1 & e * b1 = b1 ) by Lm2; ::_thesis: verum end; end; Lm3: for X being non empty compact TopSpace for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds ||.x.|| = ||.y.|| by FUNCT_1:49; Lm4: for X being non empty compact TopSpace for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 + x2 = y1 + y2 proof let X be non empty compact TopSpace; ::_thesis: for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 + x2 = y1 + y2 let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 + x2 = y1 + y2 let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 ) assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 + x2 = y1 + y2 A2: CContinuousFunctions X is add-closed by CC0SP1:def_2; A3: ComplexBoundedFunctions the carrier of X is add-closed by CC0SP1:def_2; thus x1 + x2 = ( the addF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . [x1,x2] by A2, C0SP1:def_5 .= the addF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49 .= ( the addF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49 .= y1 + y2 by A3, C0SP1:def_5 ; ::_thesis: verum end; Lm5: for X being non empty compact TopSpace for a being Complex for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y proof let X be non empty compact TopSpace; ::_thesis: for a being Complex for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y let a be Complex; ::_thesis: for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y let x be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y let y be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x = y implies a * x = a * y ) assume A1: x = y ; ::_thesis: a * x = a * y reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2; thus a * x = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . [a1,x] by CC0SP1:def_3 .= the Mult of (CAlgebra the carrier of X) . [a1,x] by FUNCT_1:49 .= ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(ComplexBoundedFunctions the carrier of X):]) . [a1,y] by A1, FUNCT_1:49 .= a * y by CC0SP1:def_3 ; ::_thesis: verum end; Lm6: for X being non empty compact TopSpace for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 * x2 = y1 * y2 proof let X be non empty compact TopSpace; ::_thesis: for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 * x2 = y1 * y2 let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 * x2 = y1 * y2 let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 * x2 = y1 * y2 ) assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 * x2 = y1 * y2 thus x1 * x2 = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . [x1,x2] by C0SP1:def_6 .= the multF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49 .= ( the multF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49 .= y1 * y2 by C0SP1:def_6 ; ::_thesis: verum end; theorem Th17: :: CC0SP2:17 for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra proof let X be non empty compact TopSpace; ::_thesis: C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1_ (C_Algebra_of_ContinuousFunctions X) ; hence C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra by CC0SP1:14; ::_thesis: verum end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital vector-distributive scalar-distributive scalar-associative vector-associative ; coherence ( C_Normed_Algebra_of_ContinuousFunctions X is right_complementable & C_Normed_Algebra_of_ContinuousFunctions X is Abelian & C_Normed_Algebra_of_ContinuousFunctions X is add-associative & C_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is associative & C_Normed_Algebra_of_ContinuousFunctions X is commutative & C_Normed_Algebra_of_ContinuousFunctions X is right-distributive & C_Normed_Algebra_of_ContinuousFunctions X is right_unital & C_Normed_Algebra_of_ContinuousFunctions X is vector-associative ) by Th17; end; theorem :: CC0SP2:18 for X being non empty compact TopSpace for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F proof let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F set X1 = CContinuousFunctions X; reconsider f1 = F as Element of CContinuousFunctions X ; A1: [1,f1] in [:COMPLEX,(CContinuousFunctions X):] by ZFMISC_1:87; (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1,F) = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . (1,f1) by CC0SP1:def_3 .= the Mult of (CAlgebra the carrier of X) . (1,f1) by A1, FUNCT_1:49 .= F by CFUNCDOM:12 ; hence (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F ; ::_thesis: verum end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is scalar-unital ) proof for v being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 1r * v = v proof let v be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 1r * v = v reconsider v1 = v as Element of CContinuousFunctions X ; A1: 1r * v = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . [1r,v1] by CC0SP1:def_3 .= the Mult of (CAlgebra the carrier of X) . (1r,v1) by FUNCT_1:49 .= v1 by CFUNCDOM:12 ; thus 1r * v = v by A1; ::_thesis: verum end; hence ( C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is scalar-unital ) by CLVECT_1:def_5; ::_thesis: verum end; end; theorem :: CC0SP2:19 for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexLinearSpace ; theorem Th20: :: CC0SP2:20 for X being non empty compact TopSpace holds X --> 0 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) proof let X be non empty compact TopSpace; ::_thesis: X --> 0 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) X --> 0 = 0. (C_Algebra_of_ContinuousFunctions X) by Th13; hence X --> 0 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ; ::_thesis: verum end; Lm7: for X being non empty compact TopSpace holds 0. (C_Normed_Algebra_of_ContinuousFunctions X) = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) proof let X be non empty compact TopSpace; ::_thesis: 0. (C_Normed_Algebra_of_ContinuousFunctions X) = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) thus 0. (C_Normed_Algebra_of_ContinuousFunctions X) = X --> 0 by Th20 .= 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by CC0SP1:18 ; ::_thesis: verum end; Lm8: for X being non empty compact TopSpace holds 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) proof let X be non empty compact TopSpace; ::_thesis: 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) thus 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1_ (C_Algebra_of_ContinuousFunctions X) .= X --> 1r by Th14 .= 1_ (C_Algebra_of_BoundedFunctions the carrier of X) by CC0SP1:9 .= 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ; ::_thesis: verum end; theorem :: CC0SP2:21 for X being non empty compact TopSpace for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.|| proof let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.|| let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 0 <= ||.F.|| reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; ||.F.|| = ||.F1.|| by FUNCT_1:49; hence 0 <= ||.F.|| by CC0SP1:20; ::_thesis: verum end; theorem Th22: :: CC0SP2:22 for X being non empty compact TopSpace for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) proof let X be non empty compact TopSpace; ::_thesis: for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) let F, G, H be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) ) reconsider f1 = F, g1 = G, h1 = H as VECTOR of (C_Algebra_of_ContinuousFunctions X) ; ( H = F + G iff h1 = f1 + g1 ) ; hence ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) ) by Th10; ::_thesis: verum end; theorem :: CC0SP2:23 for a being Complex for X being non empty compact TopSpace for f, g being Function of the carrier of X,COMPLEX for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) proof let a be Complex; ::_thesis: for X being non empty compact TopSpace for f, g being Function of the carrier of X,COMPLEX for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) let X be non empty compact TopSpace; ::_thesis: for f, g being Function of the carrier of X,COMPLEX for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) let f, g be Function of the carrier of X,COMPLEX; ::_thesis: for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) let F, G be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) ) reconsider f1 = F, g1 = G as VECTOR of (C_Algebra_of_ContinuousFunctions X) ; ( G = a * F iff g1 = a * f1 ) ; hence ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) ) by Th11; ::_thesis: verum end; theorem :: CC0SP2:24 for X being non empty compact TopSpace for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) proof let X be non empty compact TopSpace; ::_thesis: for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) let F, G, H be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) ) reconsider f1 = F, g1 = G, h1 = H as VECTOR of (C_Algebra_of_ContinuousFunctions X) ; ( H = F * G iff h1 = f1 * g1 ) ; hence ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) ) by Th12; ::_thesis: verum end; theorem Th25: :: CC0SP2:25 for X being non empty compact TopSpace holds ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 proof let X be non empty compact TopSpace; ::_thesis: ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 set F = 0. (C_Normed_Algebra_of_ContinuousFunctions X); reconsider F1 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; ( ||.F1.|| = 0 iff F1 = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25; hence ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Lm7, FUNCT_1:49; ::_thesis: verum end; theorem Th26: :: CC0SP2:26 for X being non empty compact TopSpace for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st ||.F.|| = 0 holds F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) proof let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st ||.F.|| = 0 holds F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; ( ||.F1.|| = 0 iff F1 = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25; hence ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) by Lm7, FUNCT_1:49; ::_thesis: verum end; theorem Th27: :: CC0SP2:27 for a being Complex for X being non empty compact TopSpace for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = (abs a) * ||.F.|| proof let a be Complex; ::_thesis: for X being non empty compact TopSpace for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = (abs a) * ||.F.|| let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = (abs a) * ||.F.|| let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(a * F).|| = (abs a) * ||.F.|| reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; thus ||.(a * F).|| = ||.(a * F1).|| by Lm5, Lm3 .= (abs a) * ||.F1.|| by CC0SP1:25 .= (abs a) * ||.F.|| by FUNCT_1:49 ; ::_thesis: verum end; theorem Th28: :: CC0SP2:28 for X being non empty compact TopSpace for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.|| proof let X be non empty compact TopSpace; ::_thesis: for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.|| let F, G be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(F + G).|| <= ||.F.|| + ||.G.|| reconsider F1 = F, G1 = G as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; A1: ||.F.|| = ||.F1.|| by FUNCT_1:49; A2: ||.G.|| = ||.G1.|| by FUNCT_1:49; A3: ||.(F + G).|| = ||.(F1 + G1).|| by Lm4, Lm3; thus ||.(F + G).|| <= ||.F.|| + ||.G.|| by A1, A2, A3, CC0SP1:25; ::_thesis: verum end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> discerning reflexive ComplexNormSpace-like ; coherence ( C_Normed_Algebra_of_ContinuousFunctions X is discerning & C_Normed_Algebra_of_ContinuousFunctions X is reflexive & C_Normed_Algebra_of_ContinuousFunctions X is ComplexNormSpace-like ) proof set C = C_Normed_Algebra_of_ContinuousFunctions X; A1: ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Th25; A2: for x, y being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for a being Complex holds ( ( ||.x.|| = 0 implies x = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) & ( x = 0. (C_Normed_Algebra_of_ContinuousFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th25, Th26, Th27, Th28; thus ( C_Normed_Algebra_of_ContinuousFunctions X is discerning & C_Normed_Algebra_of_ContinuousFunctions X is reflexive & C_Normed_Algebra_of_ContinuousFunctions X is ComplexNormSpace-like ) by A1, A2, CLVECT_1:def_13, NORMSP_0:def_5, NORMSP_0:def_6; ::_thesis: verum end; end; Lm9: for X being non empty compact TopSpace for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 - x2 = y1 - y2 proof let X be non empty compact TopSpace; ::_thesis: for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 - x2 = y1 - y2 let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 - x2 = y1 - y2 let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 - x2 = y1 - y2 ) assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 - x2 = y1 - y2 reconsider z2 = x2 as VECTOR of (C_Normed_Algebra_of_ContinuousFunctions X) ; reconsider e = - 1r as Complex ; - x2 = e * x2 by CLVECT_1:3 .= e * y2 by A1, Lm5 .= - y2 by CLVECT_1:3 ; hence x1 - x2 = y1 - y2 by A1, Lm4; ::_thesis: verum end; theorem :: CC0SP2:29 for X being non empty compact TopSpace for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) proof let X be non empty compact TopSpace; ::_thesis: for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) let F, G, H be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) ) assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) A2: now__::_thesis:_(_H_=_F_-_G_implies_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_) assume H = F - G ; ::_thesis: for x being Element of X holds h . x = (f . x) - (g . x) then H + G = F - (G - G) by RLVECT_1:29; then H + G = F - (0. (C_Normed_Algebra_of_ContinuousFunctions X)) by RLVECT_1:15; then A3: H + G = F by RLVECT_1:13; now__::_thesis:_for_x_being_Element_of_X_holds_(f_._x)_-_(g_._x)_=_h_._x let x be Element of X; ::_thesis: (f . x) - (g . x) = h . x f . x = (h . x) + (g . x) by A1, A3, Th22; hence (f . x) - (g . x) = h . x ; ::_thesis: verum end; hence for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)_implies_F_-_G_=_H_) assume A4: for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: F - G = H now__::_thesis:_for_x_being_Element_of_X_holds_(h_._x)_+_(g_._x)_=_f_._x let x be Element of X; ::_thesis: (h . x) + (g . x) = f . x h . x = (f . x) - (g . x) by A4; hence (h . x) + (g . x) = f . x ; ::_thesis: verum end; then F = H + G by A1, Th22; then F - G = H + (G - G) by RLVECT_1:def_3; then F - G = H + (0. (C_Normed_Algebra_of_ContinuousFunctions X)) by RLVECT_1:15; hence F - G = H by RLVECT_1:4; ::_thesis: verum end; hence ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) by A2; ::_thesis: verum end; theorem Th30: :: CC0SP2:30 for X being ComplexBanachSpace for Y being Subset of X for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds ( seq is convergent & lim seq in Y ) proof let X be ComplexBanachSpace; ::_thesis: for Y being Subset of X for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds ( seq is convergent & lim seq in Y ) let Y be Subset of X; ::_thesis: for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds ( seq is convergent & lim seq in Y ) let seq be sequence of X; ::_thesis: ( Y is closed & rng seq c= Y & seq is CCauchy implies ( seq is convergent & lim seq in Y ) ) assume A1: ( Y is closed & rng seq c= Y & seq is CCauchy ) ; ::_thesis: ( seq is convergent & lim seq in Y ) hence seq is convergent by CLOPBAN1:def_13; ::_thesis: lim seq in Y hence lim seq in Y by A1, NCFCONT1:def_3; ::_thesis: verum end; theorem Th31: :: CC0SP2:31 for X being non empty compact TopSpace for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds Y is closed proof let X be non empty compact TopSpace; ::_thesis: for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds Y is closed let Y be Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( Y = CContinuousFunctions X implies Y is closed ) assume A1: Y = CContinuousFunctions X ; ::_thesis: Y is closed now__::_thesis:_for_seq_being_sequence_of_(C_Normed_Algebra_of_BoundedFunctions_the_carrier_of_X)_st_rng_seq_c=_Y_&_seq_is_convergent_holds_ lim_seq_in_Y let seq be sequence of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( rng seq c= Y & seq is convergent implies lim seq in Y ) assume A2: ( rng seq c= Y & seq is convergent ) ; ::_thesis: lim seq in Y lim seq in ComplexBoundedFunctions the carrier of X ; then consider f being Function of the carrier of X,COMPLEX such that A3: ( f = lim seq & f | the carrier of X is bounded ) ; now__::_thesis:_for_z_being_set_st_z_in_ComplexBoundedFunctions_the_carrier_of_X_holds_ z_in_PFuncs_(_the_carrier_of_X,COMPLEX) let z be set ; ::_thesis: ( z in ComplexBoundedFunctions the carrier of X implies z in PFuncs ( the carrier of X,COMPLEX) ) assume z in ComplexBoundedFunctions the carrier of X ; ::_thesis: z in PFuncs ( the carrier of X,COMPLEX) then ex f being Function of the carrier of X,COMPLEX st ( f = z & f | the carrier of X is bounded ) ; hence z in PFuncs ( the carrier of X,COMPLEX) by PARTFUN1:45; ::_thesis: verum end; then ComplexBoundedFunctions the carrier of X c= PFuncs ( the carrier of X,COMPLEX) by TARSKI:def_3; then reconsider H = seq as Functional_Sequence of the carrier of X,COMPLEX by FUNCT_2:7; A4: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being set st n >= k & x in the carrier of X holds abs (((H . n) . x) - (f . x)) < p proof let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT for x being set st n >= k & x in the carrier of X holds abs (((H . n) . x) - (f . x)) < p ) assume p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT for x being set st n >= k & x in the carrier of X holds abs (((H . n) . x) - (f . x)) < p then consider k being Element of NAT such that A5: for n being Element of NAT st n >= k holds ||.((seq . n) - (lim seq)).|| < p by A2, CLVECT_1:def_16; take k ; ::_thesis: for n being Element of NAT for x being set st n >= k & x in the carrier of X holds abs (((H . n) . x) - (f . x)) < p hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: for x being set st n >= k & x in the carrier of X holds abs (((H . n) . x) - (f . x)) < p let x be set ; ::_thesis: ( n >= k & x in the carrier of X implies abs (((H . n) . x) - (f . x)) < p ) assume A6: ( n >= k & x in the carrier of X ) ; ::_thesis: abs (((H . n) . x) - (f . x)) < p then A7: ||.((seq . n) - (lim seq)).|| < p by A5; (seq . n) - (lim seq) in ComplexBoundedFunctions the carrier of X ; then consider g being Function of the carrier of X,COMPLEX such that A8: ( g = (seq . n) - (lim seq) & g | the carrier of X is bounded ) ; seq . n in ComplexBoundedFunctions the carrier of X ; then consider s being Function of the carrier of X,COMPLEX such that A9: ( s = seq . n & s | the carrier of X is bounded ) ; reconsider x0 = x as Element of the carrier of X by A6; A10: g . x0 = (s . x0) - (f . x0) by A8, A9, A3, CC0SP1:26; abs (g . x0) <= ||.((seq . n) - (lim seq)).|| by A8, CC0SP1:19; hence abs (((H . n) . x) - (f . x)) < p by A10, A9, A7, XXREAL_0:2; ::_thesis: verum end; end; f is continuous proof set n = the Element of NAT ; for x being Point of X for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) proof let x be Point of X; ::_thesis: for V being Subset of COMPLEX st f . x in V & V is open holds ex W being Subset of X st ( x in W & W is open & f .: W c= V ) let V be Subset of COMPLEX; ::_thesis: ( f . x in V & V is open implies ex W being Subset of X st ( x in W & W is open & f .: W c= V ) ) assume A11: ( f . x in V & V is open ) ; ::_thesis: ex W being Subset of X st ( x in W & W is open & f .: W c= V ) reconsider z0 = f . x as Complex ; consider N being Neighbourhood of z0 such that A12: N c= V by A11, CFDIFF_1:9; consider r being Real such that A13: ( 0 < r & { p where p is Complex : |.(p - z0).| < r } c= N ) by CFDIFF_1:def_5; set S = { p where p is Complex : |.(p - z0).| < r } ; A14: ( r / 3 > 0 & r / 3 is Real ) by A13, XREAL_0:def_1; consider k being Element of NAT such that A15: for n being Element of NAT for x being set st n >= k & x in the carrier of X holds abs (((H . n) . x) - (f . x)) < r / 3 by A4, A14; k in NAT ; then k in dom seq by NORMSP_1:12; then H . k in rng seq by FUNCT_1:def_3; then H . k in Y by A2; then consider h being continuous Function of the carrier of X,COMPLEX such that A16: H . k = h by A1; set z1 = h . x; set G1 = { p where p is Complex : |.(p - (h . x)).| < r / 3 } ; { p where p is Complex : |.(p - (h . x)).| < r / 3 } c= COMPLEX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { p where p is Complex : |.(p - (h . x)).| < r / 3 } or z in COMPLEX ) assume z in { p where p is Complex : |.(p - (h . x)).| < r / 3 } ; ::_thesis: z in COMPLEX then ex y being Complex st ( z = y & |.(y - (h . x)).| < r / 3 ) ; hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider T1 = { p where p is Complex : |.(p - (h . x)).| < r / 3 } as Subset of COMPLEX ; A17: T1 is open by A14, CFDIFF_1:13; |.((h . x) - (h . x)).| = 0 ; then h . x in { p where p is Complex : |.(p - (h . x)).| < r / 3 } by A13; then consider W1 being Subset of X such that A18: ( x in W1 & W1 is open & h .: W1 c= { p where p is Complex : |.(p - (h . x)).| < r / 3 } ) by A17, Th3; now__::_thesis:_for_zz0_being_set_st_zz0_in_f_.:_W1_holds_ zz0_in__{__p_where_p_is_Complex_:_|.(p_-_z0).|_<_r__}_ let zz0 be set ; ::_thesis: ( zz0 in f .: W1 implies zz0 in { p where p is Complex : |.(p - z0).| < r } ) assume zz0 in f .: W1 ; ::_thesis: zz0 in { p where p is Complex : |.(p - z0).| < r } then consider xx0 being set such that A19: ( xx0 in dom f & xx0 in W1 & f . xx0 = zz0 ) by FUNCT_1:def_6; h . xx0 in h .: W1 by A19, FUNCT_2:35; then h . xx0 in { p where p is Complex : |.(p - (h . x)).| < r / 3 } by A18; then consider hx0 being Complex such that A20: ( hx0 = h . xx0 & |.(hx0 - (h . x)).| < r / 3 ) ; |.((h . xx0) - (f . xx0)).| < r / 3 by A19, A15, A16; then |.(- ((h . xx0) - (f . xx0))).| < r / 3 by COMPLEX1:52; then A21: |.((f . xx0) - (h . xx0)).| < r / 3 ; A22: |.((h . x) - (f . x)).| < r / 3 by A15, A16; |.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).| < (r / 3) + (r / 3) by A20, A21, XREAL_1:8; then (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| < ((r / 3) + (r / 3)) + (r / 3) by A22, XREAL_1:8; then A23: (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| < r ; |.((f . xx0) - (f . x)).| = |.((((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))) + ((h . x) - (f . x))).| ; then A24: |.((f . xx0) - (f . x)).| <= |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| + |.((h . x) - (f . x)).| by COMPLEX1:56; |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| <= |.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).| by COMPLEX1:56; then |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| + |.((h . x) - (f . x)).| <= (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| by XREAL_1:6; then |.((f . xx0) - (f . x)).| <= (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| by A24, XXREAL_0:2; then |.((f . xx0) - (f . x)).| < r by A23, XXREAL_0:2; hence zz0 in { p where p is Complex : |.(p - z0).| < r } by A19; ::_thesis: verum end; then f .: W1 c= { p where p is Complex : |.(p - z0).| < r } by TARSKI:def_3; then f .: W1 c= N by A13, XBOOLE_1:1; hence ex W being Subset of X st ( x in W & W is open & f .: W c= V ) by A18, A12, XBOOLE_1:1; ::_thesis: verum end; hence f is continuous by Th3; ::_thesis: verum end; hence lim seq in Y by A3, A1; ::_thesis: verum end; hence Y is closed by NCFCONT1:def_3; ::_thesis: verum end; theorem Th32: :: CC0SP2:32 for X being non empty compact TopSpace for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds seq is convergent proof let X be non empty compact TopSpace; ::_thesis: for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds seq is convergent let vseq be sequence of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( vseq is CCauchy implies vseq is convergent ) assume A1: vseq is CCauchy ; ::_thesis: vseq is convergent A2: for x being set st x in CContinuousFunctions X holds x in ComplexBoundedFunctions the carrier of X by Lm1; then CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X by TARSKI:def_3; then rng vseq c= ComplexBoundedFunctions the carrier of X by XBOOLE_1:1; then reconsider vseq1 = vseq as sequence of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by FUNCT_2:6; now__::_thesis:_for_e_being_Real_st_e_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((vseq1_._n)_-_(vseq1_._m)).||_<_e let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq1 . n) - (vseq1 . m)).|| < e ) assume A3: e > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq1 . n) - (vseq1 . m)).|| < e consider k being Element of NAT such that A4: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A3, CSSPACE3:8; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq1 . n) - (vseq1 . m)).|| < e now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((vseq1_._n)_-_(vseq1_._m)).||_<_e let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((vseq1 . n) - (vseq1 . m)).|| < e ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((vseq1 . n) - (vseq1 . m)).|| < e then ||.((vseq . n) - (vseq . m)).|| < e by A4; hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Lm9, Lm3; ::_thesis: verum end; hence for n, m being Element of NAT st n >= k & m >= k holds ||.((vseq1 . n) - (vseq1 . m)).|| < e ; ::_thesis: verum end; then A5: vseq1 is CCauchy by CSSPACE3:8; then A6: vseq1 is convergent by CC0SP1:27; reconsider Y = CContinuousFunctions X as Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by A2, TARSKI:def_3; A7: rng vseq c= CContinuousFunctions X ; Y is closed by Th31; then reconsider tv = lim vseq1 as Point of (C_Normed_Algebra_of_ContinuousFunctions X) by A7, A5, Th30; for e being Real st e > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| < e proof let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| < e ) assume e > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| < e then consider k being Element of NAT such that A8: for n being Element of NAT st n >= k holds ||.((vseq1 . n) - (lim vseq1)).|| < e by A6, CLVECT_1:def_16; take k ; ::_thesis: for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| < e now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_ ||.((vseq_._n)_-_tv).||_<_e let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| < e ) assume n >= k ; ::_thesis: ||.((vseq . n) - tv).|| < e then ||.((vseq1 . n) - (lim vseq1)).|| < e by A8; hence ||.((vseq . n) - tv).|| < e by Lm9, Lm3; ::_thesis: verum end; hence for n being Element of NAT st n >= k holds ||.((vseq . n) - tv).|| < e ; ::_thesis: verum end; hence vseq is convergent by CLVECT_1:def_15; ::_thesis: verum end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> complete ; coherence C_Normed_Algebra_of_ContinuousFunctions X is complete proof for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds seq is convergent by Th32; hence C_Normed_Algebra_of_ContinuousFunctions X is complete by CLOPBAN1:def_13; ::_thesis: verum end; end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like ; coherence C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like proof set B = C_Normed_Algebra_of_ContinuousFunctions X; A1: now__::_thesis:_for_f,_g_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_holds_||.(f_*_g).||_<=_||.f.||_*_||.g.|| let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(f * g).|| <= ||.f.|| * ||.g.|| reconsider f1 = f, g1 = g as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; A2: ( ||.f.|| = ||.f1.|| & ||.g.|| = ||.g1.|| & ||.(f * g).|| = ||.(f1 * g1).|| ) by Lm6, Lm3; C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_1 by CC0SP1:28; hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A2, CLOPBAN2:def_9; ::_thesis: verum end; A3: C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_2 by CC0SP1:28; A4: ||.(1. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = ||.(1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by Lm8, Lm3 .= 1 by A3, CLOPBAN2:def_10 ; A5: now__::_thesis:_for_a_being_Complex for_f,_g_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_holds_a_*_(f_*_g)_=_f_*_(a_*_g) let a be Complex; ::_thesis: for f, g being Element of (C_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g) let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: a * (f * g) = f * (a * g) reconsider f1 = f, g1 = g as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; A6: a * g1 = a * g by Lm5; A7: f * g = f1 * g1 by Lm6; A8: C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_3 by CC0SP1:28; a * (f * g) = a * (f1 * g1) by A7, Lm5; then a * (f * g) = f1 * (a * g1) by A8, CLOPBAN2:def_11; hence a * (f * g) = f * (a * g) by A6, Lm6; ::_thesis: verum end; now__::_thesis:_for_f,_g,_h_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_holds_(g_+_h)_*_f_=_(g_*_f)_+_(h_*_f) let f, g, h be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: (g + h) * f = (g * f) + (h * f) reconsider f1 = f, g1 = g, h1 = h as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1; A9: g + h = g1 + h1 by Lm4; A10: ( g * f = g1 * f1 & h * f = h1 * f1 ) by Lm6; A11: C_Normed_Algebra_of_BoundedFunctions the carrier of X is left-distributive by CC0SP1:28; thus (g + h) * f = (g1 + h1) * f1 by Lm6, A9 .= (g1 * f1) + (h1 * f1) by A11, VECTSP_1:def_3 .= (g * f) + (h * f) by Lm4, A10 ; ::_thesis: verum end; then C_Normed_Algebra_of_ContinuousFunctions X is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Complex_Algebra by A1, A4, A5, CLOPBAN2:def_9, CLOPBAN2:def_10, CLOPBAN2:def_11, VECTSP_1:def_3; hence C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like ; ::_thesis: verum end; end; theorem Th33: :: CC0SP2:33 for X being non empty TopSpace for f, g being Function of the carrier of X,COMPLEX holds support (f + g) c= (support f) \/ (support g) proof let X be non empty TopSpace; ::_thesis: for f, g being Function of the carrier of X,COMPLEX holds support (f + g) c= (support f) \/ (support g) let f, g be Function of the carrier of X,COMPLEX; ::_thesis: support (f + g) c= (support f) \/ (support g) set CX = the carrier of X; set h = f + g; A1: rng (f + g) c= COMPLEX by MEMBERED:1; dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1 .= the carrier of X /\ (dom g) by PARTFUN1:def_2 .= the carrier of X /\ the carrier of X by PARTFUN1:def_2 ; then reconsider h = f + g as Function of the carrier of X,COMPLEX by A1, FUNCT_2:2; ( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def_1; then A2: ( support f c= the carrier of X & support g c= the carrier of X & support h c= the carrier of X ) by PRE_POLY:37; now__::_thesis:_for_x_being_set_st_x_in_(_the_carrier_of_X_\_(support_f))_/\_(_the_carrier_of_X_\_(support_g))_holds_ x_in_the_carrier_of_X_\_(support_(f_+_g)) let x be set ; ::_thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f + g)) ) assume x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; ::_thesis: x in the carrier of X \ (support (f + g)) then ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def_4; then ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def_5; then A3: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def_7; then (f + g) . x = (f . x) + (g . x) by VALUED_1:1 .= 0 by A3 ; then A4: ( x in the carrier of X & (f + g) . x = 0 ) by A3; not x in support (f + g) by A4, PRE_POLY:def_7; hence x in the carrier of X \ (support (f + g)) by A4, XBOOLE_0:def_5; ::_thesis: verum end; then ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f + g)) by TARSKI:def_3; then the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f + g)) by XBOOLE_1:53; then the carrier of X \ ( the carrier of X \ (support (f + g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34; then the carrier of X /\ (support (f + g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48; then the carrier of X /\ (support (f + g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48; then support (f + g) c= the carrier of X /\ ((support f) \/ (support g)) by A2, XBOOLE_1:28; then support (f + g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23; then support (f + g) c= (support f) \/ ( the carrier of X /\ (support g)) by A2, XBOOLE_1:28; hence support (f + g) c= (support f) \/ (support g) by A2, XBOOLE_1:28; ::_thesis: verum end; theorem Th34: :: CC0SP2:34 for X being non empty TopSpace for a being Complex for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f proof let X be non empty TopSpace; ::_thesis: for a being Complex for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f let a be Complex; ::_thesis: for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f let f be Function of the carrier of X,COMPLEX; ::_thesis: support (a (#) f) c= support f set CX = the carrier of X; reconsider h = a (#) f as Function of the carrier of X,COMPLEX ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (a (#) f) or x in support f ) assume x in support (a (#) f) ; ::_thesis: x in support f then (a (#) f) . x <> 0 by PRE_POLY:def_7; then a * (f . x) <> 0 by VALUED_1:6; then f . x <> 0 ; hence x in support f by PRE_POLY:def_7; ::_thesis: verum end; theorem :: CC0SP2:35 for X being non empty TopSpace for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g) proof let X be non empty TopSpace; ::_thesis: for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g) let f, g be Function of the carrier of X,COMPLEX; ::_thesis: support (f (#) g) c= (support f) \/ (support g) set CX = the carrier of X; reconsider h = f (#) g as Function of the carrier of X,COMPLEX ; ( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def_1; then A1: ( support f c= the carrier of X & support g c= the carrier of X & support h c= the carrier of X ) by PRE_POLY:37; now__::_thesis:_for_x_being_set_st_x_in_(_the_carrier_of_X_\_(support_f))_/\_(_the_carrier_of_X_\_(support_g))_holds_ x_in_the_carrier_of_X_\_(support_(f_(#)_g)) let x be set ; ::_thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f (#) g)) ) assume x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; ::_thesis: x in the carrier of X \ (support (f (#) g)) then ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def_4; then ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def_5; then A2: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def_7; (f (#) g) . x = 0 * 0 by A2, VALUED_1:5; then A3: ( x in the carrier of X & (f (#) g) . x = 0 ) by A2; not x in support (f (#) g) by A3, PRE_POLY:def_7; hence x in the carrier of X \ (support (f (#) g)) by A3, XBOOLE_0:def_5; ::_thesis: verum end; then ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f (#) g)) by TARSKI:def_3; then the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f (#) g)) by XBOOLE_1:53; then the carrier of X \ ( the carrier of X \ (support (f (#) g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34; then the carrier of X /\ (support (f (#) g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48; then the carrier of X /\ (support (f (#) g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48; then support (f (#) g) c= the carrier of X /\ ((support f) \/ (support g)) by A1, XBOOLE_1:28; then support (f (#) g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23; then support (f (#) g) c= (support f) \/ ( the carrier of X /\ (support g)) by A1, XBOOLE_1:28; hence support (f (#) g) c= (support f) \/ (support g) by A1, XBOOLE_1:28; ::_thesis: verum end; definition let X be non empty TopSpace; func CC_0_Functions X -> non empty Subset of (ComplexVectSpace the carrier of X) equals :: CC0SP2:def 7 { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } ; correctness coherence { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } is non empty Subset of (ComplexVectSpace the carrier of X); proof A1: { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } c= Funcs ( the carrier of X,COMPLEX) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } or x in Funcs ( the carrier of X,COMPLEX) ) assume x in { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } ; ::_thesis: x in Funcs ( the carrier of X,COMPLEX) then ex f being Function of the carrier of X,COMPLEX st ( x = f & f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) ; hence x in Funcs ( the carrier of X,COMPLEX) by FUNCT_2:8; ::_thesis: verum end; not { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } is empty proof set g = the carrier of X --> 0c; reconsider g = the carrier of X --> 0c as Function of the carrier of X,COMPLEX ; A2: g is continuous proof for P being Subset of COMPLEX st P is closed holds g " P is closed proof let P be Subset of COMPLEX; ::_thesis: ( P is closed implies g " P is closed ) assume P is closed ; ::_thesis: g " P is closed set F = the carrier of X --> 0; set H = the carrier of X; set HX = [#] X; percases ( 0 in P or not 0 in P ) ; suppose 0 in P ; ::_thesis: g " P is closed then g " P = [#] X by FUNCOP_1:14; hence g " P is closed ; ::_thesis: verum end; suppose not 0 in P ; ::_thesis: g " P is closed then ( the carrier of X --> 0) " P = {} X by FUNCOP_1:16; hence g " P is closed ; ::_thesis: verum end; end; end; hence g is continuous by Def1; ::_thesis: verum end; A3: ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support g holds Cl A is Subset of Y ) ) proof set S = the non empty compact Subset of X; for A being Subset of X st A = support g holds Cl A is Subset of the non empty compact Subset of X proof let A be Subset of X; ::_thesis: ( A = support g implies Cl A is Subset of the non empty compact Subset of X ) assume A4: A = support g ; ::_thesis: Cl A is Subset of the non empty compact Subset of X A5: A = {} proof assume A6: not A = {} ; ::_thesis: contradiction set p = the Element of support g; A7: the Element of support g in A by A6, A4; then g . the Element of support g <> 0 by A4, PRE_POLY:def_7; hence contradiction by A7, FUNCOP_1:7; ::_thesis: verum end; Cl ({} X) = {} by PRE_TOPC:22; hence Cl A is Subset of the non empty compact Subset of X by A5, XBOOLE_1:2; ::_thesis: verum end; hence ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support g holds Cl A is Subset of Y ) ) ; ::_thesis: verum end; g in { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } by A2, A3; hence not { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } is empty ; ::_thesis: verum end; hence { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } is non empty Subset of (ComplexVectSpace the carrier of X) by A1; ::_thesis: verum end; end; :: deftheorem defines CC_0_Functions CC0SP2:def_7_:_ for X being non empty TopSpace holds CC_0_Functions X = { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) } ; theorem :: CC0SP2:36 for X being non empty TopSpace holds CC_0_Functions X is non empty Subset of (CAlgebra the carrier of X) ; Lm10: for X being non empty TopSpace for v, u being Element of (CAlgebra the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds v + u in CC_0_Functions X proof let X be non empty TopSpace; ::_thesis: for v, u being Element of (CAlgebra the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds v + u in CC_0_Functions X set W = CC_0_Functions X; set V = CAlgebra the carrier of X; let u, v be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CC_0_Functions X & v in CC_0_Functions X implies u + v in CC_0_Functions X ) assume A1: ( u in CC_0_Functions X & v in CC_0_Functions X ) ; ::_thesis: u + v in CC_0_Functions X consider u1 being Function of the carrier of X,COMPLEX such that A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds Cl A1 is Subset of Y1 ) ) ) by A1; consider Y1 being non empty Subset of X such that A3: ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds Cl A1 is Subset of Y1 ) ) by A2; consider v1 being Function of the carrier of X,COMPLEX such that A4: ( v1 = v & v1 is continuous & ex Y2 being non empty Subset of X st ( Y2 is compact & ( for A2 being Subset of X st A2 = support v1 holds Cl A2 is Subset of Y2 ) ) ) by A1; consider Y2 being non empty Subset of X such that A5: ( Y2 is compact & ( for A2 being Subset of X st A2 = support v1 holds Cl A2 is Subset of Y2 ) ) by A4; A6: u in CContinuousFunctions X by A2; A7: v in CContinuousFunctions X by A4; CContinuousFunctions X is add-closed by CC0SP1:def_2; then v + u in CContinuousFunctions X by A6, A7, IDEAL_1:def_1; then consider fvu being continuous Function of the carrier of X,COMPLEX such that A8: v + u = fvu ; A9: Y1 \/ Y2 is compact by A3, A5, COMPTS_1:10; ( dom u1 = the carrier of X & dom v1 = the carrier of X ) by FUNCT_2:def_1; then A10: ( support u1 c= the carrier of X & support v1 c= the carrier of X ) by PRE_POLY:37; then reconsider A1 = support u1, A2 = support v1 as Subset of X ; A11: (dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1 .= the carrier of X /\ the carrier of X by FUNCT_2:def_1 .= the carrier of X ; dom (v1 + u1) = (dom v1) /\ (dom u1) by VALUED_1:def_1; then A12: support (v1 + u1) c= the carrier of X by A11, PRE_POLY:37; reconsider A1 = support u1, A2 = support v1 as Subset of X by A10; reconsider A3 = support (v1 + u1) as Subset of X by A12; A13: Cl A3 c= Cl (A2 \/ A1) by Th33, PRE_TOPC:19; A14: Cl A3 c= (Cl A2) \/ (Cl A1) by A13, PRE_TOPC:20; Cl A1 is Subset of Y1 by A3; then A15: Cl A1 c= Y1 ; Cl A2 is Subset of Y2 by A5; then (Cl A2) \/ (Cl A1) c= Y2 \/ Y1 by A15, XBOOLE_1:13; then A16: for A3 being Subset of X st A3 = support (v1 + u1) holds Cl A3 is Subset of (Y2 \/ Y1) by A14, XBOOLE_1:1; reconsider vv1 = v as Element of Funcs ( the carrier of X,COMPLEX) ; reconsider uu1 = u as Element of Funcs ( the carrier of X,COMPLEX) ; reconsider fvu1 = v + u as Element of Funcs ( the carrier of X,COMPLEX) ; A17: for x being Element of the carrier of X holds fvu1 . x = (vv1 . x) + (uu1 . x) by CFUNCDOM:1; A18: dom fvu1 = the carrier of X by FUNCT_2:def_1; for c being set st c in dom fvu1 holds fvu1 . c = (v1 . c) + (u1 . c) by A17, A2, A4; then fvu1 = v1 + u1 by A18, A11, VALUED_1:def_1; hence u + v in CC_0_Functions X by A8, A9, A16; ::_thesis: verum end; Lm11: for X being non empty TopSpace for a being Complex for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds a * u in CC_0_Functions X proof let X be non empty TopSpace; ::_thesis: for a being Complex for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds a * u in CC_0_Functions X set W = CC_0_Functions X; set V = CAlgebra the carrier of X; let a be Complex; ::_thesis: for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds a * u in CC_0_Functions X let u be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CC_0_Functions X implies a * u in CC_0_Functions X ) assume A1: u in CC_0_Functions X ; ::_thesis: a * u in CC_0_Functions X consider u1 being Function of the carrier of X,COMPLEX such that A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds Cl A1 is Subset of Y1 ) ) ) by A1; consider Y1 being non empty Subset of X such that A3: ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds Cl A1 is Subset of Y1 ) ) by A2; A4: u in CContinuousFunctions X by A2; a * u in CContinuousFunctions X by A4, CC0SP1:def_2; then consider fau being continuous Function of the carrier of X,COMPLEX such that A5: a * u = fau ; dom u1 = the carrier of X by FUNCT_2:def_1; then A6: support u1 c= the carrier of X by PRE_POLY:37; then reconsider A1 = support u1 as Subset of X ; A7: dom u1 = the carrier of X by FUNCT_2:def_1; dom (a (#) u1) = dom u1 by VALUED_1:def_5; then A8: support (a (#) u1) c= the carrier of X by A7, PRE_POLY:37; reconsider A1 = support u1 as Subset of X by A6; reconsider A3 = support (a (#) u1) as Subset of X by A8; Cl A1 is Subset of Y1 by A3; then A9: Cl A1 c= Y1 ; Cl A3 c= Cl A1 by Th34, PRE_TOPC:19; then A10: for A3 being Subset of X st A3 = support (a (#) u1) holds Cl A3 is Subset of Y1 by A9, XBOOLE_1:1; reconsider uu1 = u as Element of Funcs ( the carrier of X,COMPLEX) ; reconsider fau1 = a * u as Element of Funcs ( the carrier of X,COMPLEX) ; a in COMPLEX by XCMPLX_0:def_2; then A11: for x being Element of the carrier of X holds fau1 . x = a * (uu1 . x) by CFUNCDOM:4; A12: dom fau1 = the carrier of X by FUNCT_2:def_1; A13: dom u1 = the carrier of X by FUNCT_2:def_1; for c being set st c in dom fau1 holds fau1 . c = a * (u1 . c) by A2, A11; then fau1 = a (#) u1 by A12, A13, VALUED_1:def_5; hence a * u in CC_0_Functions X by A5, A3, A10; ::_thesis: verum end; Lm12: for X being non empty TopSpace for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds - u in CC_0_Functions X proof let X be non empty TopSpace; ::_thesis: for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds - u in CC_0_Functions X set W = CC_0_Functions X; set V = CAlgebra the carrier of X; let u be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CC_0_Functions X implies - u in CC_0_Functions X ) assume A1: u in CC_0_Functions X ; ::_thesis: - u in CC_0_Functions X set a = - 1r; - u = (- 1r) * u by CLVECT_1:3; hence - u in CC_0_Functions X by A1, Lm11; ::_thesis: verum end; theorem :: CC0SP2:37 for X being non empty TopSpace for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds W is Cadditively-linearly-closed proof let X be non empty TopSpace; ::_thesis: for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds W is Cadditively-linearly-closed let W be non empty Subset of (CAlgebra the carrier of X); ::_thesis: ( W = CC_0_Functions X implies W is Cadditively-linearly-closed ) assume A1: W = CC_0_Functions X ; ::_thesis: W is Cadditively-linearly-closed set V = CAlgebra the carrier of X; for v, u being Element of (CAlgebra the carrier of X) st v in W & u in W holds v + u in W by A1, Lm10; then A2: W is add-closed by IDEAL_1:def_1; for v being Element of (CAlgebra the carrier of X) st v in W holds - v in W by A1, Lm12; then A3: W is having-inverse by C0SP1:def_1; for a being Complex for u being Element of (CAlgebra the carrier of X) st u in W holds a * u in W by A1, Lm11; hence W is Cadditively-linearly-closed by A2, A3, CC0SP1:def_2; ::_thesis: verum end; theorem Th38: :: CC0SP2:38 for X being non empty TopSpace holds CC_0_Functions X is add-closed proof let X be non empty TopSpace; ::_thesis: CC_0_Functions X is add-closed set Y = CC_0_Functions X; set V = ComplexVectSpace the carrier of X; for v, u being VECTOR of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds v + u in CC_0_Functions X proof let v, u be VECTOR of (ComplexVectSpace the carrier of X); ::_thesis: ( v in CC_0_Functions X & u in CC_0_Functions X implies v + u in CC_0_Functions X ) assume A1: ( v in CC_0_Functions X & u in CC_0_Functions X ) ; ::_thesis: v + u in CC_0_Functions X reconsider v2 = v, u2 = u as VECTOR of (CAlgebra the carrier of X) ; v2 + u2 in CC_0_Functions X by A1, Lm10; hence v + u in CC_0_Functions X ; ::_thesis: verum end; hence CC_0_Functions X is add-closed by IDEAL_1:def_1; ::_thesis: verum end; theorem Th39: :: CC0SP2:39 for X being non empty TopSpace holds CC_0_Functions X is linearly-closed proof let X be non empty TopSpace; ::_thesis: CC_0_Functions X is linearly-closed set Y = CC_0_Functions X; set V = ComplexVectSpace the carrier of X; A1: for v, u being VECTOR of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds v + u in CC_0_Functions X proof let v, u be VECTOR of (ComplexVectSpace the carrier of X); ::_thesis: ( v in CC_0_Functions X & u in CC_0_Functions X implies v + u in CC_0_Functions X ) assume A2: ( v in CC_0_Functions X & u in CC_0_Functions X ) ; ::_thesis: v + u in CC_0_Functions X reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,COMPLEX) ; reconsider v2 = v, u2 = u as VECTOR of (CAlgebra the carrier of X) ; v2 + u2 in CC_0_Functions X by A2, Lm10; hence v + u in CC_0_Functions X ; ::_thesis: verum end; A3: for a being Complex for v being Element of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X holds a * v in CC_0_Functions X proof let a be Complex; ::_thesis: for v being Element of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X holds a * v in CC_0_Functions X let v be VECTOR of (ComplexVectSpace the carrier of X); ::_thesis: ( v in CC_0_Functions X implies a * v in CC_0_Functions X ) assume A4: v in CC_0_Functions X ; ::_thesis: a * v in CC_0_Functions X reconsider v1 = v as Element of Funcs ( the carrier of X,COMPLEX) ; reconsider v2 = v as VECTOR of (CAlgebra the carrier of X) ; a * v2 in CC_0_Functions X by A4, Lm11; hence a * v in CC_0_Functions X ; ::_thesis: verum end; thus CC_0_Functions X is linearly-closed by A1, A3, CLVECT_1:def_7; ::_thesis: verum end; registration let X be non empty TopSpace; cluster CC_0_Functions X -> non empty linearly-closed ; correctness coherence ( not CC_0_Functions X is empty & CC_0_Functions X is linearly-closed ); by Th39; end; theorem Th40: :: CC0SP2:40 for V being ComplexLinearSpace for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V proof let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed & not V1 is empty implies CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V ) assume that A1: V1 is linearly-closed and A2: not V1 is empty ; ::_thesis: CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V for v, u being VECTOR of V st v in V1 & u in V1 holds v + u in V1 by A1, CLVECT_1:def_7; then V1 is add-closed by IDEAL_1:def_1; then A3: Add_ (V1,V) = the addF of V || V1 by A2, C0SP1:def_5; A4: Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:] by A1, CSSPACE:def_9; Zero_ (V1,V) = 0. V by A1, A2, CSSPACE:def_10; hence CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V by A2, A3, A4, CLVECT_1:43; ::_thesis: verum end; theorem Th41: :: CC0SP2:41 for X being non empty TopSpace holds CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #) is Subspace of ComplexVectSpace the carrier of X by Th40; definition let X be non empty TopSpace; func C_VectorSpace_of_C_0_Functions X -> ComplexLinearSpace equals :: CC0SP2:def 8 CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #); correctness coherence CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #) is ComplexLinearSpace; by Th41; end; :: deftheorem defines C_VectorSpace_of_C_0_Functions CC0SP2:def_8_:_ for X being non empty TopSpace holds C_VectorSpace_of_C_0_Functions X = CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #); theorem Th42: :: CC0SP2:42 for X being non empty TopSpace for x being set st x in CC_0_Functions X holds x in ComplexBoundedFunctions the carrier of X proof let X be non empty TopSpace; ::_thesis: for x being set st x in CC_0_Functions X holds x in ComplexBoundedFunctions the carrier of X let x be set ; ::_thesis: ( x in CC_0_Functions X implies x in ComplexBoundedFunctions the carrier of X ) assume A1: x in CC_0_Functions X ; ::_thesis: x in ComplexBoundedFunctions the carrier of X consider f being Function of the carrier of X,COMPLEX such that A2: ( f = x & f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) by A1; consider Y being non empty Subset of X such that A3: ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) by A2; dom f = the carrier of X by FUNCT_2:def_1; then reconsider A = support f as Subset of X by PRE_POLY:37; ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) by Th8, A2; then consider f1 being Function of the carrier of X,REAL such that A4: ( f1 = |.f.| & f1 is continuous ) ; f1 .: Y is compact by A4, A3, JORDAN_A:1; then reconsider Y1 = f1 .: Y as non empty real-bounded Subset of REAL by RCOMP_1:10; A5: Y1 c= [.(inf Y1),(sup Y1).] by XXREAL_2:69; reconsider r1 = inf Y1 as real number ; reconsider r2 = sup Y1 as real number ; consider r being real number such that A6: r = ((abs r1) + (abs r2)) + 1 ; for p being Element of Y holds ( r > 0 & - r < f1 . p & f1 . p < r ) proof let p be Element of Y; ::_thesis: ( r > 0 & - r < f1 . p & f1 . p < r ) f1 . p in Y1 by FUNCT_2:35; then f1 . p in [.r1,r2.] by A5; then f1 . p in { t where t is Real : ( r1 <= t & t <= r2 ) } by RCOMP_1:def_1; then consider r3 being Element of REAL such that A7: ( r3 = f1 . p & r1 <= r3 & r3 <= r2 ) ; - (abs r1) <= r1 by ABSVALUE:4; then (- (abs r1)) - (abs r2) <= r1 - 0 by XREAL_1:13; then ((- (abs r1)) - (abs r2)) - 1 < r1 - 0 by XREAL_1:15; then A8: - r < r1 by A6; r2 <= abs r2 by ABSVALUE:4; then r2 + 0 <= (abs r2) + (abs r1) by XREAL_1:7; then A9: r2 < r by A6, XREAL_1:8; - r < f1 . p by A7, A8, XXREAL_0:2; hence ( r > 0 & - r < f1 . p & f1 . p < r ) by A7, A9, XXREAL_0:2; ::_thesis: verum end; then consider r being real number such that A10: for p being Element of Y holds ( r > 0 & - r < f1 . p & f1 . p < r ) ; for x being Point of X holds ( - r < f1 . x & f1 . x < r ) proof let x be Point of X; ::_thesis: ( - r < f1 . x & f1 . x < r ) A11: ( x in the carrier of X \ Y or x in Y ) by XBOOLE_0:def_5; percases ( x in the carrier of X \ Y or x in Y ) by A11; suppose x in the carrier of X \ Y ; ::_thesis: ( - r < f1 . x & f1 . x < r ) then A12: ( x in the carrier of X & not x in Y ) by XBOOLE_0:def_5; Cl A is Subset of Y by A3; then A13: Cl A c= Y ; support f c= Cl A by PRE_TOPC:18; then support f c= Y by A13, XBOOLE_1:1; then A14: not x in support f by A12; f . x = 0 by A14, PRE_POLY:def_7; then |.(f . x).| = 0 ; then f1 . x = 0 by A4, VALUED_1:18; hence ( - r < f1 . x & f1 . x < r ) by A10; ::_thesis: verum end; suppose x in Y ; ::_thesis: ( - r < f1 . x & f1 . x < r ) hence ( - r < f1 . x & f1 . x < r ) by A10; ::_thesis: verum end; end; end; then consider s1 being real number such that A15: for x being Point of X holds ( - s1 < f1 . x & f1 . x < s1 ) ; for y being set st y in the carrier of X /\ (dom f1) holds f1 . y <= s1 by A15; then A16: f1 | the carrier of X is bounded_above by RFUNCT_1:70; for y being set st y in the carrier of X /\ (dom f1) holds - s1 <= f1 . y by A15; then A17: f1 | the carrier of X is bounded_below by RFUNCT_1:71; the carrier of X /\ the carrier of X = the carrier of X ; then f1 | the carrier of X is bounded by A16, A17, RFUNCT_1:75; then |.(f | the carrier of X).| is bounded by A4, RFUNCT_1:46; then f | the carrier of X is bounded by CFUNCT_1:85; hence x in ComplexBoundedFunctions the carrier of X by A2; ::_thesis: verum end; definition let X be non empty TopSpace; func CC_0_FunctionsNorm X -> Function of (CC_0_Functions X),REAL equals :: CC0SP2:def 9 (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X); correctness coherence (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL; proof for x being set st x in CC_0_Functions X holds x in ComplexBoundedFunctions the carrier of X by Th42; then CC_0_Functions X c= ComplexBoundedFunctions the carrier of X by TARSKI:def_3; hence (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL by FUNCT_2:32; ::_thesis: verum end; end; :: deftheorem defines CC_0_FunctionsNorm CC0SP2:def_9_:_ for X being non empty TopSpace holds CC_0_FunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X); definition let X be non empty TopSpace; func C_Normed_Space_of_C_0_Functions X -> CNORMSTR equals :: CC0SP2:def 10 CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #); correctness coherence CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #) is CNORMSTR ; ; end; :: deftheorem defines C_Normed_Space_of_C_0_Functions CC0SP2:def_10_:_ for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X = CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #); registration let X be non empty TopSpace; cluster C_Normed_Space_of_C_0_Functions X -> non empty strict ; correctness coherence ( C_Normed_Space_of_C_0_Functions X is strict & not C_Normed_Space_of_C_0_Functions X is empty ); ; end; theorem :: CC0SP2:43 for X being non empty TopSpace for x being set st x in CC_0_Functions X holds x in CContinuousFunctions X proof let X be non empty TopSpace; ::_thesis: for x being set st x in CC_0_Functions X holds x in CContinuousFunctions X let x be set ; ::_thesis: ( x in CC_0_Functions X implies x in CContinuousFunctions X ) assume A1: x in CC_0_Functions X ; ::_thesis: x in CContinuousFunctions X consider f being Function of the carrier of X,COMPLEX such that A2: ( f = x & f is continuous & ex Y being non empty Subset of X st ( Y is compact & ( for A being Subset of X st A = support f holds Cl A is Subset of Y ) ) ) by A1; thus x in CContinuousFunctions X by A2; ::_thesis: verum end; theorem Th44: :: CC0SP2:44 for X being non empty TopSpace holds 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0 proof let X be non empty TopSpace; ::_thesis: 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0 A1: C_VectorSpace_of_C_0_Functions X is Subspace of ComplexVectSpace the carrier of X by Th41; 0. (ComplexVectSpace the carrier of X) = X --> 0 ; hence 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0 by A1, CLVECT_1:30; ::_thesis: verum end; theorem Th45: :: CC0SP2:45 for X being non empty TopSpace holds 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 proof let X be non empty TopSpace; ::_thesis: 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 0. (C_Normed_Space_of_C_0_Functions X) = 0. (C_VectorSpace_of_C_0_Functions X) .= X --> 0 by Th44 ; hence 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 ; ::_thesis: verum end; Lm13: for X being non empty TopSpace for x1, x2 being Point of (C_Normed_Space_of_C_0_Functions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 + x2 = y1 + y2 proof let X be non empty TopSpace; ::_thesis: for x1, x2 being Point of (C_Normed_Space_of_C_0_Functions X) for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 + x2 = y1 + y2 let x1, x2 be Point of (C_Normed_Space_of_C_0_Functions X); ::_thesis: for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 + x2 = y1 + y2 let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 ) A1: CC_0_Functions X is add-closed by Th38; A2: ComplexBoundedFunctions the carrier of X is add-closed by CC0SP1:def_2; assume A3: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 + x2 = y1 + y2 thus x1 + x2 = ( the addF of (ComplexVectSpace the carrier of X) || (CC_0_Functions X)) . [x1,x2] by A1, C0SP1:def_5 .= the addF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49 .= ( the addF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A3, FUNCT_1:49 .= y1 + y2 by A2, C0SP1:def_5 ; ::_thesis: verum end; Lm14: for X being non empty TopSpace for a being Complex for x being Point of (C_Normed_Space_of_C_0_Functions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y proof let X be non empty TopSpace; ::_thesis: for a being Complex for x being Point of (C_Normed_Space_of_C_0_Functions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y let a be Complex; ::_thesis: for x being Point of (C_Normed_Space_of_C_0_Functions X) for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y let x be Point of (C_Normed_Space_of_C_0_Functions X); ::_thesis: for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y let y be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x = y implies a * x = a * y ) assume A1: x = y ; ::_thesis: a * x = a * y reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2; thus a * x = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CC_0_Functions X):]) . [a1,x] by CSSPACE:def_9 .= the Mult of (CAlgebra the carrier of X) . [a1,x] by FUNCT_1:49 .= ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(ComplexBoundedFunctions the carrier of X):]) . [a1,y] by A1, FUNCT_1:49 .= a * y by CC0SP1:def_3 ; ::_thesis: verum end; theorem Th46: :: CC0SP2:46 for a being Complex for X being non empty TopSpace for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) proof let a be Complex; ::_thesis: for X being non empty TopSpace for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) let X be non empty TopSpace; ::_thesis: for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) let F, G be Point of (C_Normed_Space_of_C_0_Functions X); ::_thesis: ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) A1: ( ||.F.|| = 0 iff F = 0. (C_Normed_Space_of_C_0_Functions X) ) proof reconsider FB = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th42; A2: ||.FB.|| = ||.F.|| by FUNCT_1:49; A3: 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) = X --> 0 by CC0SP1:18; A4: 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 by Th45; ( ||.FB.|| = 0 iff FB = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25; hence ( ||.F.|| = 0 iff F = 0. (C_Normed_Space_of_C_0_Functions X) ) by A2, A3, A4; ::_thesis: verum end; A5: ||.(a * F).|| = (abs a) * ||.F.|| proof reconsider FB = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th42; A6: ||.FB.|| = ||.F.|| by FUNCT_1:49; A7: a * FB = a * F by Lm14; reconsider aFB = a * FB as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ; reconsider aF = a * F as Point of (C_Normed_Space_of_C_0_Functions X) ; A8: ||.aFB.|| = ||.aF.|| by A7, FUNCT_1:49; ||.(a * FB).|| = (abs a) * ||.FB.|| by CC0SP1:25; hence ||.(a * F).|| = (abs a) * ||.F.|| by A6, A8; ::_thesis: verum end; ||.(F + G).|| <= ||.F.|| + ||.G.|| proof A9: ( F in ComplexBoundedFunctions the carrier of X & G in ComplexBoundedFunctions the carrier of X ) by Th42; reconsider FB = F, GB = G as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by A9; A10: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49; FB + GB = F + G by Lm13; then A11: ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1:49; reconsider aFB = FB + GB as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ; reconsider aF = F, aG = G as Point of (C_Normed_Space_of_C_0_Functions X) ; ||.(FB + GB).|| <= ||.FB.|| + ||.GB.|| by CC0SP1:25; hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A10; ::_thesis: verum end; hence ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A5; ::_thesis: verum end; Lm15: for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like proof let X be non empty TopSpace; ::_thesis: C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like for x, y being Point of (C_Normed_Space_of_C_0_Functions X) for a being Complex holds ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th46; hence C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like by CLVECT_1:def_13; ::_thesis: verum end; registration let X be non empty TopSpace; cluster C_Normed_Space_of_C_0_Functions X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ; coherence ( C_Normed_Space_of_C_0_Functions X is reflexive & C_Normed_Space_of_C_0_Functions X is discerning & C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like & C_Normed_Space_of_C_0_Functions X is vector-distributive & C_Normed_Space_of_C_0_Functions X is scalar-distributive & C_Normed_Space_of_C_0_Functions X is scalar-associative & C_Normed_Space_of_C_0_Functions X is scalar-unital & C_Normed_Space_of_C_0_Functions X is Abelian & C_Normed_Space_of_C_0_Functions X is add-associative & C_Normed_Space_of_C_0_Functions X is right_zeroed & C_Normed_Space_of_C_0_Functions X is right_complementable ) proof A1: C_VectorSpace_of_C_0_Functions X is ComplexLinearSpace ; A2: for x being Point of (C_Normed_Space_of_C_0_Functions X) st ||.x.|| = 0 holds x = 0. (C_Normed_Space_of_C_0_Functions X) by Th46; ||.(0. (C_Normed_Space_of_C_0_Functions X)).|| = 0 by Th46; hence ( C_Normed_Space_of_C_0_Functions X is reflexive & C_Normed_Space_of_C_0_Functions X is discerning & C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like & C_Normed_Space_of_C_0_Functions X is vector-distributive & C_Normed_Space_of_C_0_Functions X is scalar-distributive & C_Normed_Space_of_C_0_Functions X is scalar-associative & C_Normed_Space_of_C_0_Functions X is scalar-unital & C_Normed_Space_of_C_0_Functions X is Abelian & C_Normed_Space_of_C_0_Functions X is add-associative & C_Normed_Space_of_C_0_Functions X is right_zeroed & C_Normed_Space_of_C_0_Functions X is right_complementable ) by A1, A2, Lm15, CSSPACE3:2, NORMSP_0:def_5, NORMSP_0:def_6; ::_thesis: verum end; end; theorem :: CC0SP2:47 for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace ;