let f be PartFunc of REAL,REAL; :: thesis: ( f is V8() implies f is Lipschitzian )
assume A1: f is V8() ; :: thesis: f is Lipschitzian
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 ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
then f . x1 = f . x2 by A1;
then |.((f . x1) - (f . x2)).| = 0 by ABSVALUE:2;
hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum
end;
hence f is Lipschitzian ; :: thesis: verum