let X be non empty TopSpace; :: thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX
let f, g be continuous Function of the carrier of X,COMPLEX; :: thesis: f - g is continuous Function of the carrier of X,COMPLEX
(- 1) (#) g is continuous by Th5;
hence f - g is continuous Function of the carrier of X,COMPLEX by Th4; :: thesis: verum