let a, b, c, d be Real; :: thesis: ( b > 0 & c > 0 & d > 0 & d < b implies for x being Real holds (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) )
assume that
A1: ( b > 0 & c > 0 & d > 0 ) and
A2: d < b ; :: thesis: for x being Real holds (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))
thus for x being Real holds (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) :: thesis: verum

proof

let x be Real; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))
set p = a - c;
set q = a + ((d - b) / (b / c));
set r = a + ((b - d) / (b / c));
set s = a + c;
QP: (a + ((d - b) / (b / c))) - (a - c) = ((d - b) / (b / c)) + c
.= ((d - b) * (c / b)) + c by XCMPLX_1:79
.= (((d - b) * c) / b) + c by XCMPLX_1:74
.= (((c * d) - (c * b)) / b) + c
.= (((c * d) / b) - ((c * b) / b)) + c by XCMPLX_1:120
.= (((c * d) / b) - c) + c by A1, XCMPLX_1:89
.= (c * d) / b ;
SR: (a + c) - (a + ((b - d) / (b / c))) = c - ((b - d) / (b / c))
.= c - ((b - d) * (c / b)) by XCMPLX_1:79
.= c - (((b - d) * c) / b) by XCMPLX_1:74
.= c - (((c * b) - (c * d)) / b)
.= c - (((c * b) / b) - ((c * d) / b)) by XCMPLX_1:120
.= c - (c - ((c * d) / b)) by A1, XCMPLX_1:89
.= (c * d) / b ;
d + d < b + b by A2, XREAL_1:8;
then BD: (b + b) - (d + d) > (d + d) - (d + d) by XREAL_1:14;
(a + ((b - d) / (b / c))) - (a + ((d - b) / (b / c))) = ((b - d) / (b / c)) - ((d - b) / (b / c))
.= ((b - d) - (d - b)) / (b / c) by XCMPLX_1:120
.= (((b + b) - d) - d) / (b / c) ;
then A3: ( 0 + (a - c) < ((a + ((d - b) / (b / c))) - (a - c)) + (a - c) & 0 + (a + ((d - b) / (b / c))) < ((a + ((b - d) / (b / c))) - (a + ((d - b) / (b / c)))) + (a + ((d - b) / (b / c))) & 0 + (a + ((b - d) / (b / c))) < ((a + c) - (a + ((b - d) / (b / c)))) + (a + ((b - d) / (b / c))) ) by XREAL_1:8, QP, SR, A1, BD;
BD5: ( d - b < b - b & b - d > d - d ) by A2, XREAL_1:14;
then QAR: ( a + ((d - b) / (b / c)) < a + 0 & a + 0 < a + ((b - d) / (b / c)) ) by XREAL_1:8, A1;
A4: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * ((TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c))) . x) by VALUED_1:6
.= d * ((((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) +* ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).])) . x) by FUZNUM_1:def 8, A3 ;
set Fr = AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))));
set Fs = AffineMap (0,1);
set Fl = AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))));

per cases ( a + c < x or x <= a + c ) ;

suppose B1: a + c < x ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

then ( (a + c) + (- c) < x + (- c) & (- c) + x < 0 + x ) by A1, XREAL_1:8;
then a < x by XXREAL_0:2;
then B2a: x - a > a - a by XREAL_1:14;
B3: not x in dom ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) by B1, XXREAL_1:1;
Br: a + ((b - d) / (b / c)) < x by A3, B1, XXREAL_0:2;
then B4: not x in dom ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) by XXREAL_1:1;
a + ((d - b) / (b / c)) < x by Br, A3, XXREAL_0:2;
then B5: not x in dom ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).]) by XXREAL_1:1;
( not x in ].(a - c),(a + c).[ & x in REAL ) by B1, XXREAL_1:4, XREAL_0:def 1;
then B6: x in REAL \ ].(a - c),(a + c).[ by XBOOLE_0:def 5;
BL: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * (((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) +* ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) . x) by FUNCT_4:11, B3, A4
.= d * ((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) . x) by FUNCT_4:11, B4
.= d * (((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) . x) by FUNCT_4:11, B5
.= d * ((AffineMap (0,0)) . x) by FUNCT_1:49, B6
.= d * ((0 * x) + 0) by FCONT_1:def 4 ;
x - a > (a + c) - a by XREAL_1:9, B1;
then b * (x - a) > b * c by A1, XREAL_1:68;
then (b * (x - a)) / c > (b * c) / c by A1, XREAL_1:74;
then (b * (x - a)) / c > b by A1, XCMPLX_1:89;
then BC4: ((b * (x - a)) / c) - ((b * (x - a)) / c) > b - ((b * (x - a)) / c) by XREAL_1:9;
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,(max (0,(b - ((b * (x - a)) / c))))) by ABSVALUE:def 1, B2a, A1
.= min (d,0) by BC4, XXREAL_0:def 10 ;
hence (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by BL, A1, XXREAL_0:def 9; :: thesis: verum

end;

suppose C1: x <= a + c ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

per cases ( a + ((b - d) / (b / c)) <= x or x < a + ((b - d) / (b / c)) ) ;

suppose D1: a + ((b - d) / (b / c)) <= x ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

then x in [.(a + ((b - d) / (b / c))),(a + c).] by C1;
then x in dom ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) by FUNCT_2:def 1;
then DD: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * (((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) . x) by FUNCT_4:13, A4
.= d * ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) . x) by FUNCT_1:49, XXREAL_1:1, C1, D1
.= d * (((- (1 / ((c * d) / b))) * x) + ((a + c) / ((c * d) / b))) by SR, FCONT_1:def 4
.= d * ((- ((1 / ((c * d) / b)) * x)) + ((a + c) / ((c * d) / b)))
.= d * ((- (x / ((c * d) / b))) + ((a + c) / ((c * d) / b))) by XCMPLX_1:99
.= d * (((a + c) / ((c * d) / b)) - (x / ((c * d) / b)))
.= d * (((a + c) - x) / ((c * d) / b)) by XCMPLX_1:120
.= d * (((a + c) - x) * (b / (c * d))) by XCMPLX_1:79
.= d * ((((a + c) - x) * b) / (c * d)) by XCMPLX_1:74
.= (d * (((a + c) - x) * b)) / (c * d) by XCMPLX_1:74
.= (((a + c) - x) * b) * (d / (d * c)) by XCMPLX_1:74
.= (((a + c) - x) * b) * ((d / d) / c) by XCMPLX_1:78
.= (((a + c) - x) * b) * (1 / c) by XCMPLX_1:60, A1
.= (((a + c) - x) * b) / c by XCMPLX_1:99
.= b * ((c - (x - a)) / c) by XCMPLX_1:74
.= b * ((c / c) - ((x - a) / c)) by XCMPLX_1:120
.= b * (1 - ((x - a) / c)) by A1, XCMPLX_1:60
.= (b * 1) - (b * ((x - a) / c))
.= b - ((b * (x - a)) / c) by XCMPLX_1:74 ;
D8a: (b - d) / (b / c) <= x - a by D1, XREAL_1:19;
D7: x - a > 0 by BD5, A1, D1, XREAL_1:19;
b * (x - a) <= b * c by A1, XREAL_1:64, C1, XREAL_1:20;
then (b * (x - a)) / c <= (b * c) / c by A1, XREAL_1:72;
then (b * (x - a)) / c <= b by A1, XCMPLX_1:89;
then D8: ((b * (x - a)) / c) - ((b * (x - a)) / c) <= b - ((b * (x - a)) / c) by XREAL_1:13;
((b - d) / (b / c)) * (b / c) <= (x - a) * (b / c) by A1, D8a, XREAL_1:64;
then b - d <= (x - a) * (b / c) by A1, XCMPLX_1:87;
then b <= ((x - a) * (b / c)) + d by XREAL_1:20;
then b - ((x - a) * (b / c)) <= d by XREAL_1:20;
then D9: b - ((b * (x - a)) / c) <= d by XCMPLX_1:74;
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,(max (0,(b - ((b * (x - a)) / c))))) by ABSVALUE:def 1, D7, A1
.= min (d,(b - ((b * (x - a)) / c))) by XXREAL_0:def 10, D8
.= b - ((b * (x - a)) / c) by XXREAL_0:def 9, D9 ;
hence (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by DD; :: thesis: verum

end;

suppose E1: x < a + ((b - d) / (b / c)) ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

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

suppose F1: a <= x ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

F3: not x in dom ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) by E1, XXREAL_1:1;
F4a: a + ((d - b) / (b / c)) < x by F1, XXREAL_0:2, QAR;
then x in [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).] by E1;
then F4: x in dom ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) by FUNCT_2:def 1;
EE: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * (((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) +* ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) . x) by FUNCT_4:11, F3, A4
.= d * (((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) . x) by FUNCT_4:13, F4
.= d * ((AffineMap (0,1)) . x) by FUNCT_1:49, F4a, E1, XXREAL_1:1
.= d * ((0 * x) + 1) by FCONT_1:def 4
.= d ;
F7: x - a >= a - a by F1, XREAL_1:13;
x < a + c by XXREAL_0:2, E1, A3;
then x - a < (a + c) - a by XREAL_1:14;
then b * (x - a) < b * c by A1, XREAL_1:68;
then (b * (x - a)) / c < (b * c) / c by A1, XREAL_1:74;
then (b * (x - a)) / c < b by A1, XCMPLX_1:89;
then F8: ((b * (x - a)) / c) - ((b * (x - a)) / c) < b - ((b * (x - a)) / c) by XREAL_1:14;
x - a < (a + ((b - d) / (b / c))) - a by E1, XREAL_1:14;
then (x - a) * (b / c) < ((b - d) / (b / c)) * (b / c) by A1, XREAL_1:68;
then (x - a) * (b / c) < b - d by A1, XCMPLX_1:87;
then ((x - a) * (b / c)) + d < (b - d) + d by XREAL_1:8;
then (((x - a) * (b / c)) + d) - ((x - a) * (b / c)) < b - ((x - a) * (b / c)) by XREAL_1:14;
then F9: d < b - (((x - a) * b) / c) by XCMPLX_1:74;
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,(max (0,(b - ((b * (x - a)) / c))))) by ABSVALUE:def 1, F7, A1
.= min (d,(b - ((b * (x - a)) / c))) by XXREAL_0:def 10, F8
.= d by XXREAL_0:def 9, F9 ;
hence (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by EE; :: thesis: verum

end;

suppose x < a ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

then G3: x - a < a - a by XREAL_1:14;

per cases ( a + ((d - b) / (b / c)) <= x or x < a + ((d - b) / (b / c)) ) ;

suppose H1: a + ((d - b) / (b / c)) <= x ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

F3: not x in dom ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) by E1, XXREAL_1:1;
x in [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).] by H1, E1;
then F4: x in dom ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) by FUNCT_2:def 1;
HH: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * (((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) +* ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) . x) by FUNCT_4:11, F3, A4
.= d * (((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) . x) by FUNCT_4:13, F4
.= d * ((AffineMap (0,1)) . x) by FUNCT_1:49, H1, E1, XXREAL_1:1
.= d * ((0 * x) + 1) by FCONT_1:def 4
.= d ;
(a + ((d - b) / (b / c))) - a <= x - a by XREAL_1:13, H1;
then ((d - b) / (b / c)) * (b / c) <= (x - a) * (b / c) by A1, XREAL_1:64;
then d - b <= (x - a) * (b / c) by A1, XCMPLX_1:87;
then (d - b) + b <= ((x - a) * (b / c)) + b by XREAL_1:6;
then H9: (d - b) + b <= (((x - a) * b) / c) + b by XCMPLX_1:74;
a - c < x by XXREAL_0:2, H1, A3;
then x - a > (a - c) - a by XREAL_1:14;
then b * (x - a) > b * (- c) by XREAL_1:68, A1;
then (b * (x - a)) / c > (- (c * b)) / c by A1, XREAL_1:74;
then (b * (x - a)) / c > - ((c * b) / c) by XCMPLX_1:187;
then (b * (x - a)) / c > - b by A1, XCMPLX_1:89;
then H7: ((b * (x - a)) / c) + b > (- b) + b by XREAL_1:8;
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,(max (0,(b - (- ((b * (x - a)) / c)))))) by ABSVALUE:def 1, G3, A1
.= min (d,(b + ((b * (x - a)) / c))) by XXREAL_0:def 10, H7
.= d by XXREAL_0:def 9, H9 ;
hence (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by HH; :: thesis: verum

end;

suppose I1: x < a + ((d - b) / (b / c)) ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

then ( x - (a - c) < (a + ((d - b) / (b / c))) - (a - c) & (a - c) - (a - c) < (a + ((d - b) / (b / c))) - (a - c) ) by A1, XREAL_1:14, QP;
then II: (x - (a - c)) / ((a + ((d - b) / (b / c))) - (a - c)) < ((a + ((d - b) / (b / c))) - (a - c)) / ((a + ((d - b) / (b / c))) - (a - c)) by XREAL_1:74;
I4: (AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x = ((1 / ((a + ((d - b) / (b / c))) - (a - c))) * x) + (- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))) by FCONT_1:def 4
.= (x / ((a + ((d - b) / (b / c))) - (a - c))) + (- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))) by XCMPLX_1:99
.= (x / ((a + ((d - b) / (b / c))) - (a - c))) - ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))
.= (x - (a - c)) / ((a + ((d - b) / (b / c))) - (a - c)) by XCMPLX_1:120 ;
then I3: (AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x < 1 by II, XCMPLX_1:60, QP, A1;
J8: ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x) * d < 1 * d by I3, A1, XREAL_1:68;

per cases ( a - c <= x or x < a - c ) ;

suppose J1: a - c <= x ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

x < a + ((b - d) / (b / c)) by XXREAL_0:2, A3, I1;
then J3: not x in dom ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) by XXREAL_1:1;
J4: not x in dom ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) by XXREAL_1:1, I1;
x in [.(a - c),(a + ((d - b) / (b / c))).] by I1, J1;
then J5: x in dom ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).]) by FUNCT_2:def 1;
x - a >= (a - c) - a by XREAL_1:9, J1;
then b * (x - a) >= b * (- c) by XREAL_1:64, A1;
then (b * (x - a)) / c >= (- (c * b)) / c by A1, XREAL_1:72;
then (b * (x - a)) / c >= - ((c * b) / c) by XCMPLX_1:187;
then (b * (x - a)) / c >= - b by A1, XCMPLX_1:89;
then J7: ((b * (x - a)) / c) + b >= (- b) + b by XREAL_1:6;
J9: d * ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x) = (d * (x - (a - c))) / ((c * d) / b) by XCMPLX_1:74, QP, I4
.= (d * (x - (a - c))) / (d * (c / b)) by XCMPLX_1:74
.= (x - (a - c)) / (c / b) by A1, XCMPLX_1:91
.= b * (((x - a) + c) / c) by XCMPLX_1:82 ;
JJ: min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,(max (0,(b - (- ((b * (x - a)) / c)))))) by A1, ABSVALUE:def 1, G3
.= min (d,(b + ((b * (x - a)) / c))) by XXREAL_0:def 10, J7
.= min (d,((b * 1) + (b * ((x - a) / c)))) by XCMPLX_1:74
.= min (d,(b * (1 + ((x - a) / c))))
.= min (d,(b * ((c / c) + ((x - a) / c)))) by A1, XCMPLX_1:60
.= min (d,(d * ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x))) by J9, XCMPLX_1:62
.= d * ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x) by J8, XXREAL_0:def 9 ;
(d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * (((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) +* ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) . x) by FUNCT_4:11, J3, A4
.= d * ((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) . x) by FUNCT_4:11, J4
.= d * (((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).]) . x) by FUNCT_4:13, J5
.= d * ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) . x) by FUNCT_1:49, XXREAL_1:1, I1, J1 ;
hence (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by JJ; :: thesis: verum

end;

suppose K1: x < a - c ; :: thesis: (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

then B2: x - a < (a - c) - a by XREAL_1:9;
B1: - c < 0 by A1;
b * (x - a) < b * (- c) by A1, B2, XREAL_1:68;
then (b * (x - a)) / c < (- (c * b)) / c by A1, XREAL_1:74;
then (b * (x - a)) / c < - ((c * b) / c) by XCMPLX_1:187;
then (b * (x - a)) / c < - b by A1, XCMPLX_1:89;
then B4: ((b * (x - a)) / c) + b < (- b) + b by XREAL_1:6;
KM: min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = min (d,(max (0,(b - (- ((b * (x - a)) / c)))))) by COMPLEX1:70, A1, B1, B2
.= min (d,0) by B4, XXREAL_0:def 10 ;
a - c < a + ((b - d) / (b / c)) by A3, XXREAL_0:2;
then x < a + ((b - d) / (b / c)) by K1, XXREAL_0:2;
then K3: not x in dom ((AffineMap ((- (1 / ((a + c) - (a + ((b - d) / (b / c)))))),((a + c) / ((a + c) - (a + ((b - d) / (b / c))))))) | [.(a + ((b - d) / (b / c))),(a + c).]) by XXREAL_1:1;
x < a + ((d - b) / (b / c)) by K1, A3, XXREAL_0:2;
then K4: not x in dom ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) by XXREAL_1:1;
K5: not x in dom ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).]) by K1, XXREAL_1:1;
( not x in ].(a - c),(a + c).[ & x in REAL ) by K1, XXREAL_1:4, XREAL_0:def 1;
then K6: x in REAL \ ].(a - c),(a + c).[ by XBOOLE_0:def 5;
(d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = d * (((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) +* ((AffineMap (0,1)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) . x) by FUNCT_4:11, K3, A4
.= d * ((((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) +* ((AffineMap ((1 / ((a + ((d - b) / (b / c))) - (a - c))),(- ((a - c) / ((a + ((d - b) / (b / c))) - (a - c)))))) | [.(a - c),(a + ((d - b) / (b / c))).])) . x) by FUNCT_4:11, K4
.= d * (((AffineMap (0,0)) | (REAL \ ].(a - c),(a + c).[)) . x) by FUNCT_4:11, K5
.= d * ((AffineMap (0,0)) . x) by FUNCT_1:49, K6
.= d * ((0 * x) + 0) by FCONT_1:def 4 ;
hence (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by KM, A1, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;