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

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

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

proof

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

end;

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

proof

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

end;

end;

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

end;

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