let T, S be TopSpace; :: thesis: for f being Function of T,S holds

( f is open iff ex B being Basis of T st

for V being Subset of T st V in B holds

f .: V is open )

let f be Function of T,S; :: thesis: ( f is open iff ex B being Basis of T st

for V being Subset of T st V in B holds

f .: V is open )

f .: V is open ; :: thesis: f is open

( f is open iff ex B being Basis of T st

for V being Subset of T st V in B holds

f .: V is open )

let f be Function of T,S; :: thesis: ( f is open iff ex B being Basis of T st

for V being Subset of T st V in B holds

f .: V is open )

hereby :: thesis: ( ex B being Basis of T st

for V being Subset of T st V in B holds

f .: V is open implies f is open )

given B being Basis of T such that A2:
for V being Subset of T st V in B holds for V being Subset of T st V in B holds

f .: V is open implies f is open )

assume A1:
f is open
; :: thesis: ex B being Basis of T st

for V being Subset of T st V in B holds

f .: V is open

reconsider B = the Basis of T as Basis of T ;

take B = B; :: thesis: for V being Subset of T st V in B holds

f .: V is open

let V be Subset of T; :: thesis: ( V in B implies f .: V is open )

assume V in B ; :: thesis: f .: V is open

hence f .: V is open by A1, TOPS_2:def 1, T_0TOPSP:def 2; :: thesis: verum

end;for V being Subset of T st V in B holds

f .: V is open

reconsider B = the Basis of T as Basis of T ;

take B = B; :: thesis: for V being Subset of T st V in B holds

f .: V is open

let V be Subset of T; :: thesis: ( V in B implies f .: V is open )

assume V in B ; :: thesis: f .: V is open

hence f .: V is open by A1, TOPS_2:def 1, T_0TOPSP:def 2; :: thesis: verum

f .: V is open ; :: thesis: f is open

now :: thesis: for A being Subset of T st A is open holds

f .: A is open

hence
f is open
by T_0TOPSP:def 2; :: thesis: verumf .: A is open

let A be Subset of T; :: thesis: ( A is open implies f .: A is open )

set Y = { G where G is Subset of T : ( G in B & G c= A ) } ;

{ G where G is Subset of T : ( G in B & G c= A ) } c= bool the carrier of T

set Z = { (f .: G) where G is Subset of T : G in Y } ;

{ (f .: G) where G is Subset of T : G in Y } c= bool the carrier of S

A7: for P being Subset of S st P in Z holds

P is open

then A = union Y by YELLOW_8:9;

then f .: A = union Z by RELSET_2:14;

hence f .: A is open by A7, TOPS_2:19, TOPS_2:def 1; :: thesis: verum

end;set Y = { G where G is Subset of T : ( G in B & G c= A ) } ;

{ G where G is Subset of T : ( G in B & G c= A ) } c= bool the carrier of T

proof

then reconsider Y = { G where G is Subset of T : ( G in B & G c= A ) } as Subset-Family of T ;
let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { G where G is Subset of T : ( G in B & G c= A ) } or g in bool the carrier of T )

assume g in { G where G is Subset of T : ( G in B & G c= A ) } ; :: thesis: g in bool the carrier of T

then ex G being Subset of T st

( g = G & G in B & G c= A ) ;

hence g in bool the carrier of T ; :: thesis: verum

end;assume g in { G where G is Subset of T : ( G in B & G c= A ) } ; :: thesis: g in bool the carrier of T

then ex G being Subset of T st

( g = G & G in B & G c= A ) ;

hence g in bool the carrier of T ; :: thesis: verum

set Z = { (f .: G) where G is Subset of T : G in Y } ;

{ (f .: G) where G is Subset of T : G in Y } c= bool the carrier of S

proof

then reconsider Z = { (f .: G) where G is Subset of T : G in Y } as Subset-Family of S ;
let h be object ; :: according to TARSKI:def 3 :: thesis: ( not h in { (f .: G) where G is Subset of T : G in Y } or h in bool the carrier of S )

assume h in { (f .: G) where G is Subset of T : G in Y } ; :: thesis: h in bool the carrier of S

then ex G being Subset of T st

( h = f .: G & G in Y ) ;

hence h in bool the carrier of S ; :: thesis: verum

end;assume h in { (f .: G) where G is Subset of T : G in Y } ; :: thesis: h in bool the carrier of S

then ex G being Subset of T st

( h = f .: G & G in Y ) ;

hence h in bool the carrier of S ; :: thesis: verum

A7: for P being Subset of S st P in Z holds

P is open

proof

assume
A is open
; :: thesis: f .: A is open
let P be Subset of S; :: thesis: ( P in Z implies P is open )

assume P in Z ; :: thesis: P is open

then consider G1 being Subset of T such that

A5: ( P = f .: G1 & G1 in Y ) ;

ex G2 being Subset of T st

( G1 = G2 & G2 in B & G2 c= A ) by A5;

hence P is open by A2, A5; :: thesis: verum

end;assume P in Z ; :: thesis: P is open

then consider G1 being Subset of T such that

A5: ( P = f .: G1 & G1 in Y ) ;

ex G2 being Subset of T st

( G1 = G2 & G2 in B & G2 c= A ) by A5;

hence P is open by A2, A5; :: thesis: verum

then A = union Y by YELLOW_8:9;

then f .: A = union Z by RELSET_2:14;

hence f .: A is open by A7, TOPS_2:19, TOPS_2:def 1; :: thesis: verum