let a, b, c be Real; :: thesis: ( b > 0 & c > 0 implies for x being Real holds (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).| )
assume A1: b > 0 ; :: thesis: ( not c > 0 or for x being Real holds (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).| )
assume A2: c > 0 ; :: thesis: for x being Real holds (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).|
for x being Real holds (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).|

proof

let x be Real; :: thesis: (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).|
D2: dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[) = [.a,+infty.[ by FUNCT_2:def 1;

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

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

then A31: a - x > x - x by XREAL_1:9;
A32: (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = ((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) . x by FUNCT_4:11, D2, XXREAL_1:236, A3
.= (AffineMap ((b / c),(b - ((a * b) / c)))) . x by FUNCT_1:49, A3, XXREAL_1:234
.= ((b / c) * x) + (b - ((a * b) / c)) by FCONT_1:def 4
.= ((x * b) / c) + (b - ((a * b) / c)) by XCMPLX_1:74 ;
b - |.((b * (x - a)) / c).| = b - (|.(b * (x - a)).| / |.c.|) by COMPLEX1:67
.= b - ((|.b.| * |.(x - a).|) / |.c.|) by COMPLEX1:65
.= b - ((b * |.(x - a).|) / |.c.|) by COMPLEX1:43, A1
.= b - ((b * |.(x - a).|) / c) by COMPLEX1:43, A2
.= b - ((b * |.(a - x).|) / c) by COMPLEX1:60
.= b - ((b * (a - x)) / c) by COMPLEX1:43, A31
.= b - (((b * a) - (b * x)) / c)
.= b - (((b * a) / c) - ((b * x) / c)) by XCMPLX_1:120 ;
hence (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).| by A32; :: thesis: verum

end;

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

then A41: x - a >= a - a by XREAL_1:9;
A42: (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[) . x by FUNCT_4:13, D2, XXREAL_1:236, A4
.= (AffineMap ((- (b / c)),(b + ((a * b) / c)))) . x by FUNCT_1:49, A4, XXREAL_1:236
.= ((- (b / c)) * x) + (b + ((a * b) / c)) by FCONT_1:def 4
.= (- ((b / c) * x)) + (b + ((a * b) / c))
.= (- ((x * b) / c)) + (b + ((a * b) / c)) by XCMPLX_1:74 ;
b - |.((b * (x - a)) / c).| = b - (|.(b * (x - a)).| / |.c.|) by COMPLEX1:67
.= b - ((|.b.| * |.(x - a).|) / |.c.|) by COMPLEX1:65
.= b - ((b * |.(x - a).|) / |.c.|) by COMPLEX1:43, A1
.= b - ((b * |.(x - a).|) / c) by COMPLEX1:43, A2
.= b - ((b * (x - a)) / c) by COMPLEX1:43, A41
.= b - (((b * x) - (b * a)) / c)
.= b - (((b * x) / c) - ((b * a) / c)) by XCMPLX_1:120 ;
hence (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).| by A42; :: thesis: verum

end;

end;

end;

hence for x being Real holds (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).| ; :: thesis: verum