let X be non empty TopSpace; :: thesis: C_0_Functions X is linearly-closed
set Y = C_0_Functions X;
set V = RealVectSpace the carrier of X;
A1: for v, u being VECTOR of (RealVectSpace the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds
v + u in C_0_Functions X
proof
let v, u be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in C_0_Functions X & u in C_0_Functions X implies v + u in C_0_Functions X )
assume A2: ( v in C_0_Functions X & u in C_0_Functions X ) ; :: thesis: v + u in C_0_Functions X
reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,REAL) ;
reconsider v2 = v, u2 = u as VECTOR of (RAlgebra the carrier of X) ;
v2 + u2 in C_0_Functions X by A2, Lm10;
hence v + u in C_0_Functions X ; :: thesis: verum
end;
for a being Real
for v being Element of (RealVectSpace the carrier of X) st v in C_0_Functions X holds
a * v in C_0_Functions X
proof
let a be Real; :: thesis: for v being Element of (RealVectSpace the carrier of X) st v in C_0_Functions X holds
a * v in C_0_Functions X
let v be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in C_0_Functions X implies a * v in C_0_Functions X )
assume A3: v in C_0_Functions X ; :: thesis: a * v in C_0_Functions X
reconsider v1 = v as Element of Funcs ( the carrier of X,REAL) ;
reconsider v2 = v as VECTOR of (RAlgebra the carrier of X) ;
a * v2 in C_0_Functions X by A3, Lm11;
hence a * v in C_0_Functions X ; :: thesis: verum
end;
hence C_0_Functions X is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum