let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) )
let f be Function of X,Y; :: thesis: ( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) )

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

assume A1: f is alpha-continuous ; :: thesis: ( f is s-continuous & f is (alpha,s)-continuous )
thus f is s-continuous :: thesis: f is (alpha,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 in X ^alpha by A1, Def28;
then f " V in (SO X) /\ (D(alpha,s) X) by Th12;
hence f " V in SO X by XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let G be Subset of Y; :: according to DECOMP_1:def 36 :: thesis: ( G is open implies f " G in D(alpha,s) X )
assume G is open ; :: thesis: f " G in D(alpha,s) X
then f " G in X ^alpha by A1, Def28;
then f " G in (SO X) /\ (D(alpha,s) X) by Th12;
hence f " G in D(alpha,s) X by XBOOLE_0:def 4; :: thesis: verum

end;

end;

assume A2: ( f is s-continuous & f is (alpha,s)-continuous ) ; :: thesis: f is alpha-continuous
let V be Subset of Y; :: according to DECOMP_1:def 28 :: thesis: ( V is open implies f " V in X ^alpha )
assume A3: V is open ; :: thesis: f " V in X ^alpha
then A4: f " V in SO X by A2, Def26;
f " V in D(alpha,s) X by A2, A3, Def36;
then f " V in (SO X) /\ (D(alpha,s) X) by A4, XBOOLE_0:def 4;
hence f " V in X ^alpha by Th12; :: thesis: verum