let a, b, p, q be Real; :: thesis: ( a > 0 & p > 0 implies ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) & x2 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) holds
|.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| <= r * |.(x1 - x2).| ) ) )
assume AP: ( a > 0 & p > 0 ) ; :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) & x2 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) holds
|.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| <= r * |.(x1 - x2).| ) )
set f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[);
reconsider f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) as Function of REAL,REAL by asymTT10;
f is Lipschitzian by asymTT50, AP;
hence ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) & x2 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) holds
|.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| <= r * |.(x1 - x2).| ) ) ; :: thesis: verum