let S be TopSpace; :: thesis: for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
let T be non empty TopSpace; :: thesis: for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
let BB be Basis of T; :: thesis: for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in BB holds
f " (A `) is closed )
let f be Function of S,T; :: thesis: ( f is continuous iff for A being Subset of T st A in BB holds
f " (A `) is closed )
A1: BB c= the topology of T by TOPS_2:64;

hereby :: thesis: ( ( for A being Subset of T st A in BB holds
f " (A `) is closed ) implies f is continuous )

assume A2: f is continuous ; :: thesis: for A being Subset of T st A in BB holds
f " (A `) is closed
let A be Subset of T; :: thesis: ( A in BB implies f " (A `) is closed )
assume A in BB ; :: thesis: f " (A `) is closed
then A is open by A1;
then A ` is closed by TOPS_1:4;
hence f " (A `) is closed by A2; :: thesis: verum

end;

assume A3: for A being Subset of T st A in BB holds
f " (A `) is closed ; :: thesis: f is continuous
let A be Subset of T; :: according to PRE_TOPC:def 6 :: thesis: ( not A is closed or f " A is closed )
assume A is closed ; :: thesis: f " A is closed
then A ` is open by TOPS_1:3;
then A4: A ` = union { G where G is Subset of T : ( G in BB & G c= A ` ) } by YELLOW_8:9;
set F = { (f " G) where G is Subset of T : ( G in BB & G c= A ` ) } ;
{ (f " G) where G is Subset of T : ( G in BB & G c= A ` ) } c= bool the carrier of S

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (f " G) where G is Subset of T : ( G in BB & G c= A ` ) } or a in bool the carrier of S )
assume a in { (f " G) where G is Subset of T : ( G in BB & G c= A ` ) } ; :: thesis: a in bool the carrier of S
then ex G being Subset of T st
( a = f " G & G in BB & G c= A ` ) ;
hence a in bool the carrier of S ; :: thesis: verum

end;

then reconsider F = { (f " G) where G is Subset of T : ( G in BB & G c= A ` ) } as Subset-Family of S ;
reconsider F = F as Subset-Family of S ;
F c= the topology of S

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in F or a in the topology of S )
assume a in F ; :: thesis: a in the topology of S
then consider G being Subset of T such that
A5: a = f " G and
A6: G in BB and
G c= A ` ;
A7: f " (G `) is closed by A3, A6;
(f " G) ` = f " (G `) by Th2;
then f " G is open by A7, TOPS_1:4;
hence a in the topology of S by A5; :: thesis: verum

end;

then A8: union F in the topology of S by PRE_TOPC:def 1;
defpred S₁[ Subset of T] means ( $1 in BB & $1 c= A ` );
deffunc H<sub>1</sub>( Subset of T) -> Subset of T = $1;
f " (union { H<sub>1</sub>(G) where G is Subset of T : S<sub>1</sub>[G] } ) = union { (f " H<sub>1</sub>(G)) where G is Subset of T : S<sub>1</sub>[G] } from YELLOW_9:sch 4();
then f " (A `) is open by A4, A8;
then (f " A) ` is open by Th2;
hence f " A is closed by TOPS_1:3; :: thesis: verum