let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL, the carrier of (REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
let f be PartFunc of REAL,(REAL n); :: thesis: for h being PartFunc of REAL, the carrier of (REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
let h be PartFunc of REAL, the carrier of (REAL-NS n); :: thesis: ( f = h implies ( f is Lipschitzian iff h is Lipschitzian ) )
assume AS: f = h ; :: thesis: ( f is Lipschitzian iff h is Lipschitzian )

hereby :: thesis: ( h is Lipschitzian implies f is Lipschitzian )

assume f is Lipschitzian ; :: thesis: h is Lipschitzian
then consider r being real number such that
A1: ( 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)) ) ) by Def6Th;

now

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

end;

hence h is Lipschitzian by A1, NFCONT_3:def 3; :: thesis: verum

end;

assume h is Lipschitzian ; :: thesis: f is Lipschitzian
then consider r being real number such that
A4: ( 0 < r & ( for x1, x2 being real number st x1 in dom h & x2 in dom h holds
||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) ) ) by NFCONT_3:def 3;

now

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 A6: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A4, AS;
( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by AS, REAL_NS1:def 4;
hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A6, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

end;

hence f is Lipschitzian by A4, Def6Th; :: thesis: verum