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

for A being Subset of T holds map99 .: (Cl A) c= Cl (map99 .: A)

hence map9 is continuous by JORDAN5A:27; :: thesis: verum

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

reconsider map99 = map9 as Function of T,R^1 by TOPMETR:17;
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;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

for A being Subset of T holds map99 .: (Cl A) c= Cl (map99 .: A)

proof

then
map99 is continuous
by TOPS_2:45;
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;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

hence map9 is continuous by JORDAN5A:27; :: thesis: verum