let a, b be Real; :: thesis: ( a > 0 implies |.(AffineMap (a,b)).| = (- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[) )
assume A1: a > 0 ; :: thesis: |.(AffineMap (a,b)).| = (- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)
INF: ( -infty < (- b) / a & (- b) / a < +infty ) by XXREAL_0:9, XXREAL_0:12, XREAL_0:def 1;
D1a: dom ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) = (dom (- ((AffineMap (a,b)) | ].-infty,((- b) / a).[))) \/ (dom ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) by FUNCT_4:def 1
.= ].-infty,((- b) / a).[ \/ (dom ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) by FUNCT_2:def 1
.= ].-infty,((- b) / a).[ \/ [.((- b) / a),+infty.[ by FUNCT_2:def 1
.= REAL by XXREAL_1:224, XXREAL_1:173, INF ;
for x being object st x in dom |.(AffineMap (a,b)).| holds
|.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x

proof

let x be object ; :: thesis: ( x in dom |.(AffineMap (a,b)).| implies |.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x )
assume x in dom |.(AffineMap (a,b)).| ; :: thesis: |.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x
then reconsider x = x as Real ;
A5: |.(AffineMap (a,b)).| . x = |.((AffineMap (a,b)) . x).| by VALUED_1:18
.= |.((a * x) + b).| by FCONT_1:def 4 ;

per cases ( x >= (- b) / a or x < (- b) / a ) ;

suppose A6: x >= (- b) / a ; :: thesis: |.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x

then x * a >= ((- b) / a) * a by A1, XREAL_1:64;
then x * a >= - b by A1, XCMPLX_1:87;
then A8: (a * x) + b >= (- b) + b by XREAL_1:6;
x in [.((- b) / a),+infty.[ by XXREAL_1:236, A6;
then x in dom ((AffineMap (a,b)) | [.((- b) / a),+infty.[) by FUNCT_2:def 1;
then ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x = ((AffineMap (a,b)) | [.((- b) / a),+infty.[) . x by FUNCT_4:13
.= (AffineMap (a,b)) . x by FUNCT_1:49, XXREAL_1:236, A6
.= (a * x) + b by FCONT_1:def 4 ;
hence |.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x by A5, A8, COMPLEX1:43; :: thesis: verum

end;

suppose B6: x < (- b) / a ; :: thesis: |.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x

then x * a < ((- b) / a) * a by A1, XREAL_1:68;
then x * a < - b by A1, XCMPLX_1:87;
then A8: (a * x) + b < (- b) + b by XREAL_1:6;
not x in dom ((AffineMap (a,b)) | [.((- b) / a),+infty.[) by B6, XXREAL_1:236;
then ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x = (- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) . x by FUNCT_4:11
.= - (((AffineMap (a,b)) | ].-infty,((- b) / a).[) . x) by VALUED_1:8
.= - ((AffineMap (a,b)) . x) by FUNCT_1:49, XXREAL_1:233, B6
.= - ((a * x) + b) by FCONT_1:def 4 ;
hence |.(AffineMap (a,b)).| . x = ((- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x by A5, A8, COMPLEX1:70; :: thesis: verum

end;

end;

end;

hence |.(AffineMap (a,b)).| = (- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[) by FUNCT_1:2, D1a, FUNCT_2:52; :: thesis: verum