let X be non empty TopSpace; :: thesis: CC_0_Functions X is add-closed
set Y = CC_0_Functions X;
set V = ComplexVectSpace the carrier of X;
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 A1: ( v in CC_0_Functions X & u in CC_0_Functions X ) ; :: thesis: v + u in CC_0_Functions X
reconsider v2 = v, u2 = u as VECTOR of (CAlgebra the carrier of X) ;
v2 + u2 in CC_0_Functions X by A1, Lm10;
hence v + u in CC_0_Functions X ; :: thesis: verum

end;

hence CC_0_Functions X is add-closed by IDEAL_1:def 1; :: thesis: verum