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 holds map' . x = 0

proof

assume ex x being Point of st map' . x <> 0 ; :: thesis: contradiction
then consider x being Point of 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 holds map'' .: (Cl A) c= Cl (map'' .: A)

proof

let A be Subset of ; :: 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 mCla in map'' .: (Cl A) ; :: thesis: mCla in Cl (map'' .: A)
then A5: ex Cla being set st
( Cla in dom map' & Cla in Cl A & mCla = map'' . Cla ) by FUNCT_1:def 12;
then A <> {} T by PRE_TOPC:52;
then consider a being set such that
A6: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of by A6;
( dom map' = the carrier of T & map' . a = 0 ) by A3, FUNCT_2:def 1;
then 0 in map' .: A by A6, FUNCT_1:def 12;
then A7: mCla in map' .: A by A3, A5;
map'' .: A c= Cl (map'' .: A) by PRE_TOPC:48;
hence mCla in Cl (map'' .: A) by A7; :: thesis: verum

end;

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