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 CANTOR_1:def 2;

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, PRE_TOPC:def 5;
then A ` is closed by TOPS_1:30;
hence f " (A ` ) is closed by A2, PRE_TOPC:def 12; :: 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 12 :: 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:29;
then A4: A ` = union { G where G is Subset of T : ( G in BB & G c= A ` ) } by YELLOW_8:18;
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 set ; :: 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 set ; :: 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 & G in BB & G c= A ` ) ;
( f " (G ` ) is closed & (f " G) ` = f " (G ` ) ) by A3, A5, Th2;
then f " G is open by TOPS_1:30;
hence a in the topology of S by A5, PRE_TOPC:def 5; :: thesis: verum

end;

then A6: 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, A6, PRE_TOPC:def 5;
then (f " A) ` is open by Th2;
hence f " A is closed by TOPS_1:29; :: thesis: verum