let A be non empty closed_interval Subset of REAL; :: thesis: for p, q, r, s, t, u being Real
for f being Function of REAL,REAL st p * s < 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ) holds
f is Lipschitzian
let p, q, r, s, t, u be Real; :: thesis: for f being Function of REAL,REAL st p * s < 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ) holds
f is Lipschitzian
let f be Function of REAL,REAL; :: thesis: ( p * s < 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ) implies f is Lipschitzian )
assume A1: ( p * s < 0 & p > 0 ) ; :: thesis: ( ex x being Real st not f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) or f is Lipschitzian )
assume A2: for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ; :: thesis: f is Lipschitzian
A3: p <> s by A1;
set F = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[);
reconsider F = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) as Function of REAL,REAL by FUZZY_7:12;
F is Lipschitzian by A3, FUZZY_7:42;
then consider r2 being Real such that
C1: 0 < r2 and
C2: for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.((F . x1) - (F . x2)).| <= r2 * |.(x1 - x2).| ;
C3: dom F = REAL by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1 ;
ex r1 being Real st
( 0 < r1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r1 * |.(x1 - x2).| ) )

proof

take r2 ; :: thesis: ( 0 < r2 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r2 * |.(x1 - x2).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r2 * |.(x1 - x2).|

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= r2 * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= r2 * |.(x1 - x2).|
then C3X: |.((F . x1) - (F . x2)).| <= r2 * |.(x1 - x2).| by C2, C3;
A4: |.((f . x1) - (f . x2)).| = |.((max (r,(min (u,(F . x1))))) - (f . x2)).| by A2
.= |.((max (r,(min (u,(F . x1))))) - (max (r,(min (u,(F . x2)))))).| by A2
.= |.((((r + (min (u,(F . x1)))) + |.(r - (min (u,(F . x1)))).|) / 2) - (max (r,(min (u,(F . x2)))))).| by COMPLEX1:74
.= |.((((r + (min (u,(F . x1)))) + |.(r - (min (u,(F . x1)))).|) / 2) - (((r + (min (u,(F . x2)))) + |.(r - (min (u,(F . x2)))).|) / 2)).| by COMPLEX1:74
.= |.(((((min (u,(F . x1))) + |.(r - (min (u,(F . x1)))).|) - (min (u,(F . x2)))) - |.(r - (min (u,(F . x2)))).|) * (1 / 2)).|
.= |.((((min (u,(F . x1))) - (min (u,(F . x2)))) + |.(r - (min (u,(F . x1)))).|) - |.(r - (min (u,(F . x2)))).|).| * |.(1 / 2).| by COMPLEX1:65
.= |.(((min (u,(F . x1))) - (min (u,(F . x2)))) + (|.(r - (min (u,(F . x1)))).| - |.(r - (min (u,(F . x2)))).|)).| * (1 / 2) by COMPLEX1:43 ;
A5: |.((f . x1) - (f . x2)).| <= (|.((min (u,(F . x1))) - (min (u,(F . x2)))).| + |.(|.(r - (min (u,(F . x1)))).| - |.(r - (min (u,(F . x2)))).|).|) * (1 / 2) by A4, XREAL_1:64, COMPLEX1:56;
|.(|.(r - (min (u,(F . x1)))).| - |.(r - (min (u,(F . x2)))).|).| + |.((min (u,(F . x1))) - (min (u,(F . x2)))).| <= |.((r - (min (u,(F . x1)))) - (r - (min (u,(F . x2))))).| + |.((min (u,(F . x1))) - (min (u,(F . x2)))).| by XREAL_1:6, COMPLEX1:64;
then A6s: (|.(|.(r - (min (u,(F . x1)))).| - |.(r - (min (u,(F . x2)))).|).| + |.((min (u,(F . x1))) - (min (u,(F . x2)))).|) * (1 / 2) <= (|.((r - (min (u,(F . x1)))) - (r - (min (u,(F . x2))))).| + |.((min (u,(F . x1))) - (min (u,(F . x2)))).|) * (1 / 2) by XREAL_1:64;
A7s: |.((r - (min (u,(F . x1)))) - (r - (min (u,(F . x2))))).| = |.((r - (((u + (F . x1)) - |.(u - (F . x1)).|) / 2)) - (r - (min (u,(F . x2))))).| by COMPLEX1:73
.= |.((r - (((u + (F . x1)) - |.(u - (F . x1)).|) / 2)) - (r - (((u + (F . x2)) - |.(u - (F . x2)).|) / 2))).| by COMPLEX1:73
.= |.((1 / 2) * (((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|))).|
.= |.(1 / 2).| * |.(((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).| by COMPLEX1:65
.= (1 / 2) * |.(((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).| by COMPLEX1:43 ;
|.((min (u,(F . x1))) - (min (u,(F . x2)))).| = |.((((u + (F . x1)) - |.(u - (F . x1)).|) / 2) - (min (u,(F . x2)))).| by COMPLEX1:73
.= |.((((u + (F . x1)) - |.(u - (F . x1)).|) / 2) - (((u + (F . x2)) - |.(u - (F . x2)).|) / 2)).| by COMPLEX1:73
.= |.(((((F . x1) - (F . x2)) - |.(u - (F . x1)).|) + |.(u - (F . x2)).|) * (1 / 2)).|
.= |.((((F . x1) - (F . x2)) - |.(u - (F . x1)).|) + |.(u - (F . x2)).|).| * |.(1 / 2).| by COMPLEX1:65
.= |.(((F . x1) - (F . x2)) - (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).| * (1 / 2) by COMPLEX1:43 ;
then |.((f . x1) - (f . x2)).| <= (1 / 4) * (|.(((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).| + |.(- (((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|))).|) by A7s, A6s, A5, XXREAL_0:2;
then A8s: |.((f . x1) - (f . x2)).| <= (1 / 4) * (|.(((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).| + |.(((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).|) by COMPLEX1:52;
(1 / 2) * |.(((F . x2) - (F . x1)) + (|.(u - (F . x1)).| - |.(u - (F . x2)).|)).| <= (1 / 2) * (|.((F . x2) - (F . x1)).| + |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).|) by XREAL_1:64, COMPLEX1:56;
then A9: |.((f . x1) - (f . x2)).| <= (1 / 2) * (|.((F . x2) - (F . x1)).| + |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).|) by A8s, XXREAL_0:2;
|.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).| <= |.((u - (F . x1)) - (u - (F . x2))).| by COMPLEX1:64;
then |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).| <= |.(- ((F . x1) - (F . x2))).| ;
then |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).| <= |.((F . x1) - (F . x2)).| by COMPLEX1:52;
then |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).| + |.((F . x1) - (F . x2)).| <= |.((F . x1) - (F . x2)).| + |.((F . x1) - (F . x2)).| by XREAL_1:6;
then (1 / 2) * (|.(- ((F . x2) - (F . x1))).| + |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).|) <= (1 / 2) * (2 * |.((F . x1) - (F . x2)).|) by XREAL_1:64;
then (1 / 2) * (|.((F . x2) - (F . x1)).| + |.(|.(u - (F . x1)).| - |.(u - (F . x2)).|).|) <= (1 / 2) * (2 * |.((F . x1) - (F . x2)).|) by COMPLEX1:52;
then |.((f . x1) - (f . x2)).| <= (1 / 2) * (2 * |.((F . x1) - (F . x2)).|) by XXREAL_0:2, A9;
hence |.((f . x1) - (f . x2)).| <= r2 * |.(x1 - x2).| by XXREAL_0:2, C3X; :: thesis: verum

end;

hence ( 0 < r2 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r2 * |.(x1 - x2).| ) ) by C1; :: thesis: verum

end;

hence f is Lipschitzian ; :: thesis: verum