let f be PartFunc of REAL,REAL; :: thesis: ( ( for x0 being Real st x0 in dom f holds
f . x0 = x0 ) implies f is continuous )
assume A1: for x0 being Real st x0 in dom f holds
f . x0 = x0 ; :: thesis: f is continuous
now :: thesis: for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
f . x1 = x1 by A1, A2;
hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by A1, A3; :: thesis: verum
end;
then f is Lipschitzian ;
hence f is continuous ; :: thesis: verum