let a, b be Real; :: thesis: AffineMap (a,b) is Lipschitzian
set f = AffineMap (a,b);
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (AffineMap (a,b)) & x2 in dom (AffineMap (a,b)) holds
|.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= r * |.(x1 - x2).| ) )

proof

take |.a.| + 1 ; :: thesis: ( 0 < |.a.| + 1 & ( for x1, x2 being Real st x1 in dom (AffineMap (a,b)) & x2 in dom (AffineMap (a,b)) holds
|.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= (|.a.| + 1) * |.(x1 - x2).| ) )
|.a.| >= 0 by COMPLEX1:46;
hence |.a.| + 1 > 0 ; :: thesis: for x1, x2 being Real st x1 in dom (AffineMap (a,b)) & x2 in dom (AffineMap (a,b)) holds
|.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= (|.a.| + 1) * |.(x1 - x2).|
thus for x1, x2 being Real st x1 in dom (AffineMap (a,b)) & x2 in dom (AffineMap (a,b)) holds
|.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= (|.a.| + 1) * |.(x1 - x2).| :: thesis: verum

proof

let x1, x2 be Real; :: thesis: ( x1 in dom (AffineMap (a,b)) & x2 in dom (AffineMap (a,b)) implies |.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= (|.a.| + 1) * |.(x1 - x2).| )
assume ( x1 in dom (AffineMap (a,b)) & x2 in dom (AffineMap (a,b)) ) ; :: thesis: |.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= (|.a.| + 1) * |.(x1 - x2).|
B2: |.a.| + 1 > |.a.| + 0 by XREAL_1:8;
BB: |.(x1 - x2).| >= 0 by COMPLEX1:46;
|.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| = |.(((a * x1) + b) - ((AffineMap (a,b)) . x2)).| by FCONT_1:def 4
.= |.(((a * x1) + b) - ((a * x2) + b)).| by FCONT_1:def 4
.= |.(a * (x1 - x2)).|
.= |.a.| * |.(x1 - x2).| by COMPLEX1:65 ;
hence |.(((AffineMap (a,b)) . x1) - ((AffineMap (a,b)) . x2)).| <= (|.a.| + 1) * |.(x1 - x2).| by XREAL_1:64, B2, BB; :: thesis: verum

end;

end;

hence AffineMap (a,b) is Lipschitzian ; :: thesis: verum