let X be non empty TopSpace; :: thesis: for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds
- u in CC_0_Functions X
set W = CC_0_Functions X;
set V = CAlgebra the carrier of X;
let u be Element of (CAlgebra the carrier of X); :: thesis: ( u in CC_0_Functions X implies - u in CC_0_Functions X )
assume A1: u in CC_0_Functions X ; :: thesis: - u in CC_0_Functions X
set a = - 1r;
- u = (- 1r) * u by CLVECT_1:3;
hence - u in CC_0_Functions X by A1, Lm11; :: thesis: verum