let f be PartFunc of REAL,REAL; :: thesis: ( f is empty implies f is Lipschitzian )

assume A1: f is empty ; :: thesis: f is Lipschitzian

take 1 ; :: according to FCONT_1:def 3 :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )

thus ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) by A1; :: thesis: verum

assume A1: f is empty ; :: thesis: f is Lipschitzian

take 1 ; :: according to FCONT_1:def 3 :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )

thus ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) by A1; :: thesis: verum