let n be Element of NAT ; :: thesis: for X being set
for f being PartFunc of REAL,(REAL n) holds
( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) )
let X be set ; :: thesis: for f being PartFunc of REAL,(REAL n) holds
( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) )
let f be PartFunc of REAL,(REAL n); :: thesis: ( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) )

hereby :: thesis: ( ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) implies f | X is Lipschitzian )

assume f | X is Lipschitzian ; :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) )
then consider r being Real such that
A1: ( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).| ) ) by Th33;
take r = r; :: thesis: ( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) )
thus 0 < r by A1; :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).|
thus for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| :: thesis: verum

proof

let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| )
assume A2: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).|
then |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).| by A1;
then |.((f /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).| by A2, PARTFUN2:15;
hence |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A2, PARTFUN2:15; :: thesis: verum

end;

end;

given r being Real such that A3: ( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) ; :: thesis: f | X is Lipschitzian

now :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).| )
assume A4: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).|
then |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A3;
then |.(((f | X) /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A4, PARTFUN2:15;
hence |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * |.(x1 - x2).| by A4, PARTFUN2:15; :: thesis: verum

end;

hence f | X is Lipschitzian by A3, Th33; :: thesis: verum