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 A2: a < 0 ; :: thesis: |.(AffineMap (a,b)).| = ((AffineMap (a,b)) | ].-infty,((- b) / a).[) +* (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[))
set f = ((AffineMap (a,b)) | ].-infty,((- b) / a).[) +* (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[));
A1: ( dom (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) = [.((- b) / a),+infty.[ & [.((- b) / a),+infty.[ = dom ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) ) by FUNCT_2:def 1;
for x being object st x in dom ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) holds
(- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x = ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) . x

proof

let x be object ; :: thesis: ( x in dom ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) implies (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x = ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) . x )
assume A3: x in dom ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) ; :: thesis: (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x = ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) . x
hence ((- (AffineMap (a,b))) | [.((- b) / a),+infty.[) . x = (- (AffineMap (a,b))) . x by FUNCT_1:49
.= - ((AffineMap (a,b)) . x) by VALUED_1:8
.= - (((AffineMap (a,b)) | [.((- b) / a),+infty.[) . x) by FUNCT_1:49, A3
.= (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x by VALUED_1:8 ;
:: thesis: verum

end;

then - ((AffineMap (a,b)) | [.((- b) / a),+infty.[) = (- (AffineMap (a,b))) | [.((- b) / a),+infty.[ by FUNCT_1:2, A1;
then reconsider f = ((AffineMap (a,b)) | ].-infty,((- b) / a).[) +* (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) as Function of REAL,REAL by FUZZY_6:18;
for x being Element of REAL holds f . x = |.(AffineMap (a,b)).| . x

proof

let x be Element of REAL ; :: thesis: f . x = |.(AffineMap (a,b)).| . x

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

suppose A6: x >= (- b) / a ; :: thesis: f . x = |.(AffineMap (a,b)).| . x

then x * a <= ((- b) / a) * a by A2, XREAL_1:65;
then x * a <= - b by A2, 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;
hence f . x = (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) . x by FUNCT_4:13
.= - (((AffineMap (a,b)) | [.((- b) / a),+infty.[) . x) by VALUED_1:8
.= - ((AffineMap (a,b)) . x) by FUNCT_1:49, XXREAL_1:236, A6
.= - ((a * x) + b) by FCONT_1:def 4
.= |.((a * x) + b).| by COMPLEX1:70, A8
.= |.((AffineMap (a,b)) . x).| by FCONT_1:def 4
.= |.(AffineMap (a,b)).| . x by VALUED_1:18 ;
:: thesis: verum

end;

suppose B5: x < (- b) / a ; :: thesis: f . x = |.(AffineMap (a,b)).| . x

then x * a > ((- b) / a) * a by A2, XREAL_1:69;
then x * a > - b by A2, XCMPLX_1:87;
then B8: (a * x) + b > (- b) + b by XREAL_1:6;
not x in dom (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[)) by B5, XXREAL_1:236;
hence f . x = ((AffineMap (a,b)) | ].-infty,((- b) / a).[) . x by FUNCT_4:11
.= (AffineMap (a,b)) . x by FUNCT_1:49, XXREAL_1:233, B5
.= (a * x) + b by FCONT_1:def 4
.= |.((a * x) + b).| by COMPLEX1:43, B8
.= |.((AffineMap (a,b)) . x).| by FCONT_1:def 4
.= |.(AffineMap (a,b)).| . x by VALUED_1:18 ;
:: thesis: verum

end;

end;

end;

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