let X be non empty TopSpace; :: thesis: for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds
W is Cadditively-linearly-closed
let W be non empty Subset of (CAlgebra the carrier of X); :: thesis: ( W = CC_0_Functions X implies W is Cadditively-linearly-closed )
assume A1: W = CC_0_Functions X ; :: thesis: W is Cadditively-linearly-closed
set V = CAlgebra the carrier of X;
for v, u being Element of (CAlgebra the carrier of X) st v in W & u in W holds
v + u in W by A1, Lm10;
then A2: W is add-closed by IDEAL_1:def 1;
for v being Element of (CAlgebra the carrier of X) st v in W holds
- v in W by A1, Lm12;
then A3: W is having-inverse by C0SP1:def 1;
for a being Complex
for u being Element of (CAlgebra the carrier of X) st u in W holds
a * u in W by A1, Lm11;
hence W is Cadditively-linearly-closed by A2, A3; :: thesis: verum