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 that
AP: a <> p and
AF: f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) ; :: thesis: f is Lipschitzian
set fa = AffineMap (a,b);
set fp = AffineMap (p,q);
B1: a - p <> 0 by AP;
A1: AffineMap (a,b) is Lipschitzian by Th21;
A2: AffineMap (p,q) is Lipschitzian by Th21;
B2: (AffineMap (a,b)) . ((q - b) / (a - p)) = (a * ((q - b) / (a - p))) + b by FCONT_1:def 4
.= ((a * (q - b)) / (a - p)) + b by XCMPLX_1:74
.= ((a * (q - b)) + ((a - p) * b)) / (a - p) by XCMPLX_1:113, B1 ;
(AffineMap (p,q)) . ((q - b) / (a - p)) = (p * ((q - b) / (a - p))) + q by FCONT_1:def 4
.= ((p * (q - b)) / (a - p)) + q by XCMPLX_1:74
.= ((p * (q - b)) + ((a - p) * q)) / (a - p) by XCMPLX_1:113, B1 ;
hence f is Lipschitzian by Th20, AF, A1, A2, B2; :: thesis: verum