let a, b, p, q be Real; :: thesis: for f being Function of REAL,REAL st a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) holds
f is Lipschitzian
let f be Function of REAL,REAL; :: thesis: ( a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) implies f is Lipschitzian )
assume A1: ( a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) ) ; :: thesis: f is Lipschitzian
then f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) by FUZZY_6:35;
hence f is Lipschitzian by FUZZY_6:28, A1; :: thesis: verum