let X be non empty TopSpace; :: thesis: for W being non empty Subset of (RAlgebra the carrier of X) st W = C_0_Functions X holds
W is additively-linearly-closed
let W be non empty Subset of (RAlgebra the carrier of X); :: thesis: ( W = C_0_Functions X implies W is additively-linearly-closed )
assume A1: W = C_0_Functions X ; :: thesis: W is additively-linearly-closed
set V = RAlgebra the carrier of X;
for v, u being Element of (RAlgebra 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 (RAlgebra the carrier of X) st v in W holds
- v in W by A1, Lm12;
then A3: W is having-inverse ;
for a being Real
for u being Element of (RAlgebra the carrier of X) st u in W holds
a * u in W by A1, Lm11;
hence W is additively-linearly-closed by A2, A3; :: thesis: verum