let X be non empty TopSpace; for a being Real
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X
set W = C_0_Functions X;
set V = RAlgebra the carrier of X;
let a be Real; for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X
let u be Element of (RAlgebra the carrier of X); ( u in C_0_Functions X implies a * u in C_0_Functions X )
assume A1:
u in C_0_Functions X
; a * u 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;
A4:
u in ContinuousFunctions X
by A2;
reconsider aa = a as Real ;
aa * u in ContinuousFunctions X
by A4, C0SP1:def 10;
then consider fau being continuous RealMap of X such that
A5:
fau = a * u
;
A6:
dom u1 = the carrier of X
by FUNCT_2:def 1;
then reconsider A1 = support u1 as Subset of X by PRE_POLY:37;
A7:
dom u1 = the carrier of X
by FUNCT_2:def 1;
A8:
dom (a (#) u1) = dom u1
by VALUED_1:def 5;
reconsider A1 = support u1 as Subset of X by A6, PRE_POLY:37;
reconsider A3 = support (a (#) u1) as Subset of X by A8, A7, PRE_POLY:37;
A9:
Cl A1 is Subset of Y1
by A3;
Cl A3 c= Cl A1
by Th24, PRE_TOPC:19;
then A10:
for A3 being Subset of X st A3 = support (a (#) u1) holds
Cl A3 is Subset of Y1
by A9, XBOOLE_1:1;
reconsider uu1 = u as Element of Funcs ( the carrier of X,REAL) ;
reconsider fau1 = a * u as Element of Funcs ( the carrier of X,REAL) ;
A11:
dom fau1 = the carrier of X
by FUNCT_2:def 1;
A12:
dom u1 = the carrier of X
by FUNCT_2:def 1;
for c being object st c in dom fau1 holds
fau1 . c = a * (u1 . c)
by A2, FUNCSDOM:4;
then
fau1 = a (#) u1
by A11, A12, VALUED_1:def 5;
hence
a * u in C_0_Functions X
by A3, A10, A5; verum