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

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

assume f is Lipschitzian ; :: thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) )
then consider g being PartFunc of REAL, the carrier of (REAL-NS n) such that
A1: ( g = f & g is Lipschitzian ) by Def6;
consider r being real number such that
A2: ( 0 < r & ( for x1, x2 being real number st x1 in dom g & x2 in dom g holds
||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) ) ) by A1, NFCONT_3:def 3;
take r = r; :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) )
thus 0 < r by A2; :: thesis: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
thus for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) :: thesis: verum

proof

let x1, x2 be real number ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2))
then A4: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A1, A2;
( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by A1, REAL_NS1:def 4;
hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

end;

end;

given r being real number such that A5: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ; :: thesis: f is Lipschitzian
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;

now

let x1, x2 be real number ; :: thesis: ( x1 in dom g & x2 in dom g implies ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) )
assume ( x1 in dom g & x2 in dom g ) ; :: thesis: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2))
then A7: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A5;
( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by REAL_NS1:def 4;
hence ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A7, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

end;

then g is Lipschitzian by A5, NFCONT_3:def 3;
hence f is Lipschitzian by Def6; :: thesis: verum