:: deftheorem Def3 defines Lipschitzian PDIFF_6:def 3 :
for m, n being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ) );