let f be Function of S,T; :: thesis: ( f is constant implies f is continuous )
assume A1: f is constant ; :: thesis: f is continuous

per cases ( S is empty or not S is empty ) ;

suppose A2: S is empty ; :: thesis: f is continuous

for P1 being Subset of T st P1 is closed holds
f " P1 is closed by A2;
hence f is continuous by PRE_TOPC:def 6; :: thesis: verum

end;

suppose not S is empty ; :: thesis: f is continuous

then consider y being Element of T such that
A3: rng f = {y} by A1, FUNCT_2:111;
y in rng f by A3, TARSKI:def 1;
then ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
then A4: the_value_of f = y by A1, FUNCT_1:def 12;
f = (dom f) --> (the_value_of f) by A1, FUNCOP_1:80;
then f = S --> y by A4, FUNCT_2:def 1;
hence f is continuous ; :: thesis: verum

end;

end;