let X, Y be TopStruct ; :: thesis: for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
( f is continuous iff for P being Subset of Y st P is open holds
f " P is open )
let f be Function of X,Y; :: thesis: ( ( [#] Y = {} implies [#] X = {} ) implies ( f is continuous iff for P being Subset of Y st P is open holds
f " P is open ) )
assume A1: ( [#] Y = {} implies [#] X = {} ) ; :: thesis: ( f is continuous iff for P being Subset of Y st P is open holds
f " P is open )
assume A4: for P1 being Subset of Y st P1 is open holds
f " P1 is open ; :: thesis: f is continuous
let P1 be Subset of Y; :: according to PRE_TOPC:def 6 :: thesis: ( not P1 is closed or f " P1 is closed )
assume P1 is closed ; :: thesis: f " P1 is closed
then P1 ` is open ;
then A5: f " (P1 `) is open by A4;
f " (P1 `) = (f " ([#] Y)) \ (f " P1) by FUNCT_1:69
.= ([#] X) \ (f " P1) by A1, Th41
.= (f " P1) ` ;
hence f " P1 is closed by A5; :: thesis: verum