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

now

reconsider s = 1 as real number ;
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
A2: x0 in dom f and
A3: 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 ) )
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 A4: 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 A1, A2, A4, FUNCT_1:def 10;
hence abs ((f . x1) - (f . x0)) < r by A3, ABSVALUE:2; :: thesis: verum

end;

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