let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for a being Real
for u being Element of (RealVectSpace ( the carrier of X,T)) st u in C_0_Functions (X,T) holds
a * u in C_0_Functions (X,T)
let T be NormedLinearTopSpace; :: thesis: for a being Real
for u being Element of (RealVectSpace ( the carrier of X,T)) st u in C_0_Functions (X,T) holds
a * u in C_0_Functions (X,T)
set W = C_0_Functions (X,T);
set V = RealVectSpace ( the carrier of X,T);
let a be Real; :: thesis: for u being Element of (RealVectSpace ( the carrier of X,T)) st u in C_0_Functions (X,T) holds
a * u in C_0_Functions (X,T)
let u be Element of (RealVectSpace ( the carrier of X,T)); :: thesis: ( u in C_0_Functions (X,T) implies a * u in C_0_Functions (X,T) )
assume u in C_0_Functions (X,T) ; :: thesis: a * u in C_0_Functions (X,T)
then 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 ) ) ;
consider Y1 being non empty Subset of X such that
A3: ( Y1 is compact & Cl (support u1) c= Y1 ) by A2;
A4: u in ContinuousFunctions (X,T) by A2;
ContinuousFunctions (X,T) is linearly-closed by Th5;
then a * u in ContinuousFunctions (X,T) by A4;
then consider fau being Function of the carrier of X, the carrier of T such that
A5: ( a * u = fau & fau is continuous ) ;
A6: dom fau = the carrier of X by FUNCT_2:def 1;
A7: dom u1 = the carrier of X by FUNCT_2:def 1;
Cl (support (a (#) u1)) c= Cl (support u1) by Th55, PRE_TOPC:19;
then A8: Cl (support (a (#) u1)) c= Y1 by A3;
for x being Element of X st x in dom fau holds
fau /. x = a * (u1 /. x) by LOPBAN_1:12, A2, A5;
then fau = a (#) u1 by VFUNCT_1:def 4, A7, A6;
hence a * u in C_0_Functions (X,T) by A3, A8, A5; :: thesis: verum