let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )
let f be Function of X,Y; :: thesis: ( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )
A1: [#] Y <> {} ;

hereby :: thesis: ( f is ps-continuous & f is (c,ps)-continuous implies f is continuous )

assume A2: f is continuous ; :: thesis: ( f is ps-continuous & f is (c,ps)-continuous )
thus f is ps-continuous :: thesis: f is (c,ps)-continuous

proof

let V be Subset of Y; :: according to DECOMP_1:def 29 :: thesis: ( V is open implies f " V in PSO X )
assume V is open ; :: thesis: f " V in PSO X
then f " V is open by A1, A2, TOPS_2:43;
then f " V in the topology of X by PRE_TOPC:def 2;
then f " V in (PSO X) /\ (D(c,ps) X) by Th10;
hence f " V in PSO X by XBOOLE_0:def 4; :: thesis: verum

end;

thus f is (c,ps)-continuous :: thesis: verum

proof

let V be Subset of Y; :: according to DECOMP_1:def 34 :: thesis: ( V is open implies f " V in D(c,ps) X )
assume V is open ; :: thesis: f " V in D(c,ps) X
then f " V is open by A1, A2, TOPS_2:43;
then f " V in the topology of X by PRE_TOPC:def 2;
then f " V in (PSO X) /\ (D(c,ps) X) by Th10;
hence f " V in D(c,ps) X by XBOOLE_0:def 4; :: thesis: verum

end;

end;

assume A3: ( f is ps-continuous & f is (c,ps)-continuous ) ; :: thesis: f is continuous

now :: thesis: for V being Subset of Y st V is open holds
f " V is open

let V be Subset of Y; :: thesis: ( V is open implies f " V is open )
assume V is open ; :: thesis: f " V is open
then ( f " V in PSO X & f " V in D(c,ps) X ) by A3;
then f " V in (PSO X) /\ (D(c,ps) X) by XBOOLE_0:def 4;
then f " V in the topology of X by Th10;
hence f " V is open by PRE_TOPC:def 2; :: thesis: verum

end;

hence f is continuous by A1, TOPS_2:43; :: thesis: verum