:: deftheorem defines Lipschitzian NFCONT_4:def 6 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex g being PartFunc of REAL,(REAL-NS n) st
( g = f & g is Lipschitzian ) );