let X be non empty TopSpace; :: thesis: for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
- u in C_0_Functions X
set W = C_0_Functions X;
set V = RAlgebra the carrier of X;
let u be Element of (RAlgebra the carrier of X); :: thesis: ( u in C_0_Functions X implies - u in C_0_Functions X )
assume A1: u in C_0_Functions X ; :: thesis: - u in C_0_Functions X
set a = - 1;
RAlgebra the carrier of X is RealLinearSpace by C0SP1:7;
then - u = (- 1) * u by RLVECT_1:16;
hence - u in C_0_Functions X by Lm11, A1; :: thesis: verum