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 object 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