let f be PartFunc of REAL ,REAL ; :: thesis: ( f is constant implies f is continuous )
assume Z1: f is constant ; :: thesis: f is continuous

now

let x0, r be real number ; :: thesis: ( x0 in dom f & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume that
Z2: x0 in dom f and
Z3: 0 < r ; :: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
reconsider s = 1 as real number ;
take s = s; :: thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
thus 0 < s ; :: thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r
let x1 be real number ; :: thesis: ( x1 in dom f & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume Z4: x1 in dom f ; :: thesis: ( abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume abs (x1 - x0) < s ; :: thesis: abs ((f . x1) - (f . x0)) < r
f . x1 = f . x0 by Z1, Z2, Z4, FUNCT_1:def 16;
hence abs ((f . x1) - (f . x0)) < r by Z3, ABSVALUE:7; :: thesis: verum

end;

then f | (dom f) is continuous by Th15;
hence f is continuous by RELAT_1:98; :: thesis: verum