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 map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds
map9 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 map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds
map9 is continuous )
assume A1: for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ; :: thesis: for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds
map9 is continuous
set F = Funcs ( the carrier of T,REAL);
let map9 be Element of Funcs ( the carrier of T,REAL); :: thesis: ( map9 is_a_unity_wrt ADD implies map9 is continuous )
assume A2: map9 is_a_unity_wrt ADD ; :: thesis: map9 is continuous
A3: for x being Point of T holds map9 . x = 0
proof
assume ex x being Point of T st map9 . x <> 0 ; :: thesis: contradiction
then consider x being Point of T such that
A4: map9 . x <> 0 ;
ADD . (map9,map9) = map9 by A2, BINOP_1:3;
then map9 + map9 = map9 by A1;
then (map9 . x) + (map9 . x) = map9 . x by Def7;
hence contradiction by A4; :: thesis: verum
end;
reconsider map99 = map9 as Function of T,R^1 by TOPMETR:17;
for A being Subset of T holds map99 .: (Cl A) c= Cl (map99 .: A)
proof
let A be Subset of T; :: thesis: map99 .: (Cl A) c= Cl (map99 .: A)
let mCla be object ; :: according to TARSKI:def 3 :: thesis: ( not mCla in map99 .: (Cl A) or mCla in Cl (map99 .: A) )
assume mCla in map99 .: (Cl A) ; :: thesis: mCla in Cl (map99 .: A)
then A5: ex Cla being object st
( Cla in dom map9 & Cla in Cl A & mCla = map99 . Cla ) by FUNCT_1:def 6;
then A <> {} T by PRE_TOPC:22;
then consider a being object such that
A6: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of T by A6;
( dom map9 = the carrier of T & map9 . a = 0 ) by A3, FUNCT_2:def 1;
then 0 in map9 .: A by A6, FUNCT_1:def 6;
then A7: mCla in map9 .: A by A3, A5;
map99 .: A c= Cl (map99 .: A) by PRE_TOPC:18;
hence mCla in Cl (map99 .: A) by A7; :: thesis: verum
end;
then map99 is continuous by TOPS_2:45;
hence map9 is continuous by JORDAN5A:27; :: thesis: verum