let r3 be Real; :: thesis: for T being TopStruct
for f being RealMap of T st f is continuous holds
r3 + f is continuous
let T be TopStruct ; :: thesis: for f being RealMap of T st f is continuous holds
r3 + f is continuous
let f be RealMap of T; :: thesis: ( f is continuous implies r3 + f is continuous )
assume A1: f is continuous ; :: thesis: r3 + f is continuous
let X be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis: ( X is closed implies (r3 + f) " X is closed )
assume X is closed ; :: thesis: (r3 + f) " X is closed
then A2: (- r3) ++ X is closed by MEASURE6:53;
(r3 + f) " X = f " ((- r3) ++ X) by MEASURE6:70;
hence (r3 + f) " X is closed by A1, A2; :: thesis: verum