let T, S be TopSpace; :: thesis: for f being Function of T,S holds
( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )
let f be Function of T,S; :: thesis: ( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )
hereby :: thesis: ( ( for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ) implies f is continuous )
assume A1: f is continuous ; :: thesis: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1)
let P1 be Subset of S; :: thesis: Cl (f " P1) c= f " (Cl P1)
Cl (Cl P1) = Cl P1 ;
then Cl P1 is closed by PRE_TOPC:22;
then A2: f " (Cl P1) is closed by A1;
f " P1 c= f " (Cl P1) by PRE_TOPC:18, RELAT_1:143;
then Cl (f " P1) c= Cl (f " (Cl P1)) by PRE_TOPC:19;
hence Cl (f " P1) c= f " (Cl P1) by A2, PRE_TOPC:22; :: thesis: verum
end;
assume A3: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ; :: thesis: f is continuous
let P1 be Subset of S; :: 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 Cl P1 = P1 by PRE_TOPC:22;
then ( f " P1 c= Cl (f " P1) & Cl (f " P1) c= f " P1 ) by A3, PRE_TOPC:18;
then f " P1 = Cl (f " P1) by XBOOLE_0:def 10;
hence f " P1 is closed by PRE_TOPC:22; :: thesis: verum