let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for v, u being Element of (RealVectSpace ( the carrier of X,T)) st v in C_0_Functions (X,T) & u in C_0_Functions (X,T) holds
v + u in C_0_Functions (X,T)
let T be NormedLinearTopSpace; :: thesis: for v, u being Element of (RealVectSpace ( the carrier of X,T)) st v in C_0_Functions (X,T) & u in C_0_Functions (X,T) holds
v + u in C_0_Functions (X,T)
set W = C_0_Functions (X,T);
set V = RealVectSpace ( the carrier of X,T);
let u, v be Element of (RealVectSpace ( the carrier of X,T)); :: thesis: ( u in C_0_Functions (X,T) & v in C_0_Functions (X,T) implies u + v in C_0_Functions (X,T) )
assume A1: ( u in C_0_Functions (X,T) & v in C_0_Functions (X,T) ) ; :: thesis: u + v in C_0_Functions (X,T)
consider u1 being Function of the carrier of X, the carrier of T such that
A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st
( Y1 is compact & Cl (support u1) c= Y1 ) ) by A1;
consider Y1 being non empty Subset of X such that
A3: ( Y1 is compact & Cl (support u1) c= Y1 ) by A2;
consider v1 being Function of the carrier of X, the carrier of T such that
A4: ( v1 = v & v1 is continuous & ex Y2 being non empty Subset of X st
( Y2 is compact & Cl (support v1) c= Y2 ) ) by A1;
consider Y2 being non empty Subset of X such that
A5: ( Y2 is compact & Cl (support v1) c= Y2 ) by A4;
A6: ContinuousFunctions (X,T) is linearly-closed by Th5;
A7: u in ContinuousFunctions (X,T) by A2;
v in ContinuousFunctions (X,T) by A4;
then v + u in ContinuousFunctions (X,T) by A7, A6;
then consider fvu being Function of the carrier of X, the carrier of T such that
A9: ( v + u = fvu & fvu is continuous ) ;
reconsider Y12 = Y1 \/ Y2 as non empty Subset of X ;
A10: Y12 is compact by A3, A5, COMPTS_1:10;
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 ;
Cl (support (v1 + u1)) c= Cl ((support u1) \/ (support v1)) by Th54, PRE_TOPC:19;
then A12: Cl (support (v1 + u1)) c= (Cl (support u1)) \/ (Cl (support v1)) by PRE_TOPC:20;
(Cl (support v1)) \/ (Cl (support u1)) c= Y1 \/ Y2 by A3, A5, XBOOLE_1:13;
then A13: Cl (support (v1 + u1)) c= Y12 by A12;
A14: dom fvu = the carrier of X by FUNCT_2:def 1;
for x being Element of X st x in dom fvu holds
fvu /. x = (v1 /. x) + (u1 /. x) by LOPBAN_1:11, A9, A2, A4;
then fvu = v1 + u1 by VFUNCT_1:def 1, A14, A11;
hence u + v in C_0_Functions (X,T) by A9, A10, A13; :: thesis: verum