let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL, the carrier of S; :: thesis: ( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
thus ( f | X is Lipschitzian implies ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) ) :: thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian )

proof

given r being real number such that A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) ; :: according to NFCONT_3:def 3 :: thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) )
take r ; :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) )
thus 0 < r by A1; :: thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) )
B: ( x1 in REAL & x2 in REAL ) by XREAL_0:def 1;
assume A3: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2))
then ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by PARTFUN2:15, B;
hence ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) by A2, A3; :: thesis: verum

end;

given r being real number such that A4: 0 < r and
A5: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ; :: thesis: f | X is Lipschitzian
take r ; :: according to NFCONT_3:def 3 :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) ) )
thus 0 < r by A4; :: thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) )
B: ( x1 in REAL & x2 in REAL ) by XREAL_0:def 1;
assume A6: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2))
then ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by PARTFUN2:15, B;
hence ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) by A5, A6; :: thesis: verum