let T be TopStruct ; :: thesis: for S being non empty TopStruct
for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
let S be non empty TopStruct ; :: thesis: for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
let f be Function of T,S; :: thesis: for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open
let H be Subset-Family of S; :: thesis: ( f is continuous & H is open implies for F being Subset-Family of T st F = (" f) .: H holds
F is open )
assume that
A1: f is continuous and
A2: H is open ; :: thesis: for F being Subset-Family of T st F = (" f) .: H holds
F is open
let F be Subset-Family of T; :: thesis: ( F = (" f) .: H implies F is open )
assume A3: F = (" f) .: H ; :: thesis: F is open
let X be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( X in F implies X is open )
assume X in F ; :: thesis: X is open
then consider y being object such that
A4: y in dom (" f) and
A5: y in H and
A6: X = (" f) . y by A3, FUNCT_1:def 6;
reconsider Y = y as Subset of S by A5;
A7: X = f " Y by A4, A6, FUNCT_3:21;
A8: ( [#] S = {} implies [#] T = {} ) ;
Y is open by A2, A5;
hence X is open by A1, A8, A7, Th43; :: thesis: verum