let X be non empty TopSpace; :: thesis: CC_0_Functions X is linearly-closed
set Y = CC_0_Functions X;
set V = ComplexVectSpace the carrier of X;
A1: for v, u being VECTOR of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds
v + u in CC_0_Functions X

proof

let v, u be VECTOR of (ComplexVectSpace the carrier of X); :: thesis: ( v in CC_0_Functions X & u in CC_0_Functions X implies v + u in CC_0_Functions X )
assume A2: ( v in CC_0_Functions X & u in CC_0_Functions X ) ; :: thesis: v + u in CC_0_Functions X
reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider v2 = v, u2 = u as VECTOR of (CAlgebra the carrier of X) ;
v2 + u2 in CC_0_Functions X by A2, Lm10;
hence v + u in CC_0_Functions X ; :: thesis: verum

end;

A3: for a being Complex
for v being Element of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X holds
a * v in CC_0_Functions X

proof

let a be Complex; :: thesis: for v being Element of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X holds
a * v in CC_0_Functions X
let v be VECTOR of (ComplexVectSpace the carrier of X); :: thesis: ( v in CC_0_Functions X implies a * v in CC_0_Functions X )
assume A4: v in CC_0_Functions X ; :: thesis: a * v in CC_0_Functions X
reconsider v1 = v as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider v2 = v as VECTOR of (CAlgebra the carrier of X) ;
a * v2 in CC_0_Functions X by A4, Lm11;
hence a * v in CC_0_Functions X ; :: thesis: verum

end;

thus CC_0_Functions X is linearly-closed by A1, A3; :: thesis: verum