let f be PartFunc of REAL ,REAL ; :: thesis: ( ( for x0 being real number st x0 in dom f holds
f . x0 = abs x0 ) implies f is continuous )
assume A1: for x0 being real number st x0 in dom f holds
f . x0 = abs x0 ; :: thesis: f is continuous

now

let x1, x2 be real number ; :: thesis: ( x1 in dom f & x2 in dom f implies abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2))
then ( f . x1 = abs x1 & f . x2 = abs x2 ) by A1;
hence abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) by COMPLEX1:150; :: thesis: verum

end;

then f is Lipschitzian by XDef3;
hence f is continuous ; :: thesis: verum