let S be TopSpace; :: thesis: for T being non empty TopSpace
for K being prebasis 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 prebasis 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 prebasis 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
reconsider C = FinMeetCl BB as Basis of T by Th23;

now :: thesis: for A being Subset of T st A in C holds
f " (A `) is closed

let A be Subset of T; :: thesis: ( A in C implies f " (A `) is closed )
assume A in C ; :: thesis: f " (A `) is closed
then consider Y being Subset-Family of T such that
A4: Y c= BB and
A5: Y is finite and
A6: A = Intersect Y by CANTOR_1:def 3;
reconsider Y = Y as Subset-Family of T ;
reconsider CY = COMPLEMENT Y as Subset-Family of T ;
defpred S₁[ set ] means $1 in Y;
deffunc H₁( Subset of T) -> Element of bool the carrier of T = $1 ` ;
A7: f " (A `) = f " (union CY) by A6, YELLOW_8:7
.= f " (union { H₁(a) where a is Subset of T : S₁[a] } ) by Th3
.= union { (f " H₁(y)) where y is Subset of T : S₁[y] } from YELLOW_9:sch 4() ;
set X = { (f " (y `)) where y is Subset of T : y in Y } ;
{ (f " (y `)) where y is Subset of T : y in Y } c= bool the carrier of S

proof

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

end;

then reconsider X = { (f " (y `)) where y is Subset of T : y in Y } as Subset-Family of S ;
reconsider X = X as Subset-Family of S ;
A8: X is closed

proof

let a be Subset of S; :: according to TOPS_2:def 2 :: thesis: ( not a in X or a is closed )
assume a in X ; :: thesis: a is closed
then ex y being Subset of T st
( a = f " (y `) & y in Y ) ;
hence a is closed by A3, A4; :: thesis: verum

end;

A9: Y is finite by A5;
deffunc H₂( Subset of T) -> Element of bool the carrier of S = f " ($1 `);
{ H<sub>2</sub>(y) where y is Subset of T : y in Y } is finite from FRAENKEL:sch 21(A9);
hence f " (A `) is closed by A7, A8, TOPS_2:21; :: thesis: verum

end;

hence f is continuous by Th33; :: thesis: verum