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

assume A1: f is constant ; :: thesis: f is continuous

assume A1: f is constant ; :: thesis: f is continuous

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

end;

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;f " P1 is closed by A2;

hence f is continuous by PRE_TOPC:def 6; :: thesis: verum

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;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