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

hence f is continuous ; :: thesis: verum

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).|

then
f is Lipschitzian
;|.((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 ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

then ( f . x1 = |.x1.| & f . x2 = |.x2.| ) by A1;

hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:64; :: thesis: verum

end;assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

then ( f . x1 = |.x1.| & f . x2 = |.x2.| ) by A1;

hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:64; :: thesis: verum

hence f is continuous ; :: thesis: verum