let X be non empty TopSpace; :: thesis: for a being Complex
for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds
a * u in CC_0_Functions X
set W = CC_0_Functions X;
set V = CAlgebra the carrier of X;
let a be Complex; :: thesis: for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds
a * u in CC_0_Functions X
let u be Element of (CAlgebra the carrier of X); :: thesis: ( u in CC_0_Functions X implies a * u in CC_0_Functions X )
assume A1: u in CC_0_Functions X ; :: thesis: a * u 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;
A4: u in CContinuousFunctions X by A2;
a * u in CContinuousFunctions X by A4, CC0SP1:def 2;
then consider fau being continuous Function of the carrier of X,COMPLEX such that
A5: a * u = fau ;
dom u1 = the carrier of X by FUNCT_2:def 1;
then A6: support u1 c= the carrier of X by PRE_POLY:37;
then reconsider A1 = support u1 as Subset of X ;
A7: dom u1 = the carrier of X by FUNCT_2:def 1;
dom (a (#) u1) = dom u1 by VALUED_1:def 5;
then A8: support (a (#) u1) c= the carrier of X by A7, PRE_POLY:37;
reconsider A1 = support u1 as Subset of X by A6;
reconsider A3 = support (a (#) u1) as Subset of X by A8;
Cl A1 is Subset of Y1 by A3;
then A9: Cl A1 c= Y1 ;
Cl A3 c= Cl A1 by Th34, 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,COMPLEX) ;
reconsider fau1 = a * u as Element of Funcs ( the carrier of X,COMPLEX) ;
A11: for x being Element of the carrier of X holds fau1 . x = a * (uu1 . x) by CFUNCDOM:4;
A12: dom fau1 = the carrier of X by FUNCT_2:def 1;
A13: 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, A11;
then fau1 = a (#) u1 by A12, A13, VALUED_1:def 5;
hence a * u in CC_0_Functions X by A5, A3, A10; :: thesis: verum