let X be non empty TopSpace; :: thesis: for v, u being Element of (RAlgebra the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds
v + u in C_0_Functions X
set W = C_0_Functions X;
set V = RAlgebra the carrier of X;
let u, v be Element of (RAlgebra the carrier of X); :: thesis: ( u in C_0_Functions X & v in C_0_Functions X implies u + v in C_0_Functions X )
assume A1: ( u in C_0_Functions X & v in C_0_Functions X ) ; :: thesis: u + v in C_0_Functions X
consider u1 being RealMap of X 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 RealMap of X 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 ContinuousFunctions X by A2;
A7: v in ContinuousFunctions X by A4;
v + u in ContinuousFunctions X by A6, A7, IDEAL_1:def 1;
then consider fvu being continuous RealMap of X such that
A8: v + u = fvu ;
A9: Y1 \/ Y2 is compact by A3, A5, COMPTS_1:10;
A10: ( dom u1 = the carrier of X & dom v1 = the carrier of X ) by FUNCT_2:def 1;
reconsider A1 = support u1, A2 = support v1 as Subset of X by A10, PRE_POLY:37;
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 ;
A12: dom (v1 + u1) = (dom v1) /\ (dom u1) by VALUED_1:def 1;
reconsider A1 = support u1, A2 = support v1 as Subset of X by A10, PRE_POLY:37;
reconsider A3 = support (v1 + u1) as Subset of X by A12, A11, PRE_POLY:37;
Cl A3 c= Cl (A2 \/ A1) by Th23, PRE_TOPC:19;
then A13: Cl A3 c= (Cl A2) \/ (Cl A1) by PRE_TOPC:20;
A14: Cl A1 is Subset of Y1 by A3;
Cl A2 is Subset of Y2 by A5;
then (Cl A2) \/ (Cl A1) c= Y2 \/ Y1 by A14, XBOOLE_1:13;
then A15: for A3 being Subset of X st A3 = support (v1 + u1) holds
Cl A3 is Subset of (Y2 \/ Y1) by A13, XBOOLE_1:1;
reconsider vv1 = v as Element of Funcs ( the carrier of X,REAL) ;
reconsider uu1 = u as Element of Funcs ( the carrier of X,REAL) ;
reconsider fvu1 = v + u as Element of Funcs ( the carrier of X,REAL) ;
A16: dom fvu1 = the carrier of X by FUNCT_2:def 1;
for c being object st c in dom fvu1 holds
fvu1 . c = (v1 . c) + (u1 . c) by A2, A4, FUNCSDOM:1;
then fvu1 = v1 + u1 by A16, A11, VALUED_1:def 1;
hence u + v in C_0_Functions X by A8, A9, A15; :: thesis: verum