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

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

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

proof

let V be Subset of Y; :: according to DECOMP_1:def 26 :: thesis: ( V is open implies f " V in SO X )
assume V is open ; :: thesis: f " V in SO 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 (SO X) /\ (D(c,s) X) by Th8;
hence f " V in SO X by XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let V be Subset of Y; :: according to DECOMP_1:def 32 :: thesis: ( V is open implies f " V in D(c,s) X )
assume V is open ; :: thesis: f " V in D(c,s) 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 (SO X) /\ (D(c,s) X) by Th8;
hence f " V in D(c,s) X by XBOOLE_0:def 4; :: thesis: verum

end;

end;

assume A3: ( f is s-continuous & f is (c,s)-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 SO X & f " V in D(c,s) X ) by A3;
then f " V in (SO X) /\ (D(c,s) X) by XBOOLE_0:def 4;
then f " V in the topology of X by Th8;
hence f " V is open by PRE_TOPC:def 2; :: thesis: verum

end;

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