let a, b, c, d be Real; :: thesis:
assume A1: ( a < b & b < c & c < d ) ; :: thesis:
set a1 = 1 / (b - a);
set b1 = - (a / (b - a));
set p1 = 1 / (d - c);
set q1 = d / (d - c);
A20: a - a < b - a by XREAL_1:9, A1;
A30: c - c < d - c by XREAL_1:9, A1;
B1: (- (- (a / (b - a)))) / (1 / (b - a)) = (b - a) * ((a / (b - a)) / 1) by XCMPLX_1:81
.= a by XCMPLX_1:87, A20 ;
B2: (1 - (- (a / (b - a)))) / (1 / (b - a)) = (1 + (a / (b - a))) * (b - a) by XCMPLX_1:100
.= (b - a) + ((a / (b - a)) * (b - a))
.= (b - a) + a by XCMPLX_1:87, A20
.= b ;
B3: (1 - (d / (d - c))) / (- (1 / (d - c))) = - ((1 - (d / (d - c))) / (1 / (d - c))) by XCMPLX_1:188
.= - ((1 - (d / (d - c))) * (d - c)) by XCMPLX_1:100
.= - ((1 * (d - c)) - ((d / (d - c)) * (d - c)))
.= - ((d - c) - d) by XCMPLX_1:87, A30
.= c ;
B4: d = (d - c) * ((d / (d - c)) / 1) by A30, XCMPLX_1:87
.= (d / (d - c)) / (1 / (d - c)) by XCMPLX_1:81 ;
((d / (d - c)) - (- (a / (b - a)))) / ((1 / (b - a)) + (1 / (d - c))) = ((d / (d - c)) + (a / (b - a))) / ((1 / (b - a)) + (1 / (d - c)))
.= (((d * (b - a)) + (a * (d - c))) / ((d - c) * (b - a))) / ((1 / (b - a)) + (1 / (d - c))) by XCMPLX_1:116, A20, A30
.= (((((d * b) - (d * a)) + (a * d)) - (a * c)) / ((d - c) * (b - a))) / (((1 * (b - a)) + (1 * (d - c))) / ((d - c) * (b - a))) by XCMPLX_1:116, A20, A30
.= ((b * d) - (a * c)) / (((d - c) + b) - a) by XCMPLX_1:55, A20, A30 ;
hence for x being Real holds (TrapezoidalFS (a,b,c,d)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,(((b * d) - (a * c)) / (((d - c) + b) - a)).[) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.(((b * d) - (a * c)) / (((d - c) + b) - a)),+infty.[)) . x)))) by B1, B4, asymTT7, A20, A30, B2, B3, A1; :: thesis: