let f be Function of REAL,REAL; :: thesis: for a, b, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) holds
f is Lipschitzian
let a, b, r, s be Real; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) implies f is Lipschitzian )
assume A1: for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ; :: thesis: f is Lipschitzian
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

proof

per cases ( a = 0 or a <> 0 ) ;

suppose C0: a = 0 ; :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

take 1 ; :: 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).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by A1
.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by FCONT_1:def 4
.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((a * x2) + b)))))).| by FCONT_1:def 4
.= 0 by COMPLEX1:44, C0 ;
hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum

end;

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

end;

suppose A2: a <> 0 ; :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

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

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).|
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by A1
.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by FCONT_1:def 4
.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((a * x2) + b)))))).| by FCONT_1:def 4 ;
then |.((f . x1) - (f . x2)).| <= |.(((a * x1) + b) - ((a * x2) + b)).| by LeMM01;
then |.((f . x1) - (f . x2)).| <= |.(a * (x1 - x2)).| ;
hence |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| by COMPLEX1:65; :: thesis: verum

end;

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

end;

end;

end;

hence f is Lipschitzian ; :: thesis: verum