let T be non empty TopSpace; :: thesis: for ADD being BinOp of (Funcs the carrier of T,REAL ) st ( for f1, f2 being RealMap of T holds ADD . f1,f2 = f1 + f2 ) holds
for map' being Element of Funcs the carrier of T,REAL st map' is_a_unity_wrt ADD holds
map' is continuous
let ADD be BinOp of (Funcs the carrier of T,REAL ); :: thesis: ( ( for f1, f2 being RealMap of T holds ADD . f1,f2 = f1 + f2 ) implies for map' being Element of Funcs the carrier of T,REAL st map' is_a_unity_wrt ADD holds
map' is continuous )
assume A1: for f1, f2 being RealMap of T holds ADD . f1,f2 = f1 + f2 ; :: thesis: for map' being Element of Funcs the carrier of T,REAL st map' is_a_unity_wrt ADD holds
map' is continuous
set F = Funcs the carrier of T,REAL ;
let map' be Element of Funcs the carrier of T,REAL ; :: thesis: ( map' is_a_unity_wrt ADD implies map' is continuous )
assume A2: map' is_a_unity_wrt ADD ; :: thesis: map' is continuous
A3: for x being Point of T holds map' . x = 0

proof

assume ex x being Point of T st map' . x <> 0 ; :: thesis: contradiction
then consider x being Point of T such that
A4: map' . x <> 0 ;
ADD . map',map' = map' by A2, BINOP_1:11;
then map' + map' = map' by A1;
then (map' . x) + (map' . x) = map' . x by Def7;
hence contradiction by A4; :: thesis: verum

end;

reconsider map'' = map' as Function of T,R^1 by TOPMETR:24;
for A being Subset of T holds map'' .: (Cl A) c= Cl (map'' .: A)

proof

let A be Subset of T; :: thesis: map'' .: (Cl A) c= Cl (map'' .: A)
let mCla be set ; :: according to TARSKI:def 3 :: thesis: ( not mCla in map'' .: (Cl A) or mCla in Cl (map'' .: A) )
assume A5: mCla in map'' .: (Cl A) ; :: thesis: mCla in Cl (map'' .: A)
consider Cla being set such that
A6: ( Cla in dom map' & Cla in Cl A & mCla = map'' . Cla ) by A5, FUNCT_1:def 12;
A <> {} T by A6, PRE_TOPC:52;
then consider a being set such that
A7: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of T by A7;
dom map' = the carrier of T by FUNCT_2:def 1;
then ( a in dom map' & a in A & map' . a = 0 ) by A3, A7;
then ( 0 in map' .: A & 0 = mCla ) by A3, A6, FUNCT_1:def 12;
then ( mCla in map' .: A & map'' .: A c= Cl (map'' .: A) ) by PRE_TOPC:48;
hence mCla in Cl (map'' .: A) ; :: thesis: verum

end;

then map'' is continuous by TOPS_2:57;
hence map' is continuous by TOPREAL6:83; :: thesis: verum