let X be 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
set W = CC_0_Functions X;
set V = CAlgebra the carrier of X;
let u, v be Element of (CAlgebra the carrier of X); ( 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 )
; 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; verum