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 )

hereby :: thesis: ( ( for P being Subset of Y st P is open holds
f " P is open ) implies f is continuous )

assume A2: f is continuous ; :: thesis: for P1 being Subset of Y st P1 is open holds
f " P1 is open
let P1 be Subset of Y; :: thesis: ( P1 is open implies f " P1 is open )
assume P1 is open ; :: thesis: f " P1 is open
then P1 ` is closed by TOPS_1:4;
then A3: f " (P1 `) is closed by A2;
f " (P1 `) = (f " ([#] Y)) \ (f " P1) by FUNCT_1:69
.= ([#] X) \ (f " P1) by A1, Th41
.= (f " P1) ` ;
hence f " P1 is open by A3, TOPS_1:4; :: thesis: verum

end;

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