let a, b, c, d be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f | [.(a - c),(a + c).] = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies f | [.(a - c),(a + c).] = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).]) )
assume that
A1: ( b > 0 & c > 0 & d > 0 ) and
A2: d < b and
A3: for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: f | [.(a - c),(a + c).] = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])
- ((b - d) / (b / c)) > - c by XREAL_1:24, Lmbcd, A1;
then A5a: (- (b - d)) / (b / c) > - c by XCMPLX_1:187;
then A5: (- c) + a < ((d - b) / (b / c)) + a by XREAL_1:8;
A60: ( d - b < b - b & b - d > d - d ) by A2, XREAL_1:9;
then A6: a + ((d - b) / (b / c)) < a + ((b - d) / (b / c)) by XREAL_1:6, A1;
(b - d) / (b / c) < c by Lmbcd, A1;
then A7: ((b - d) / (b / c)) + a < c + a by XREAL_1:8;
A8: a - c < a + ((b - d) / (b / c)) by A60, A5, XREAL_1:6, A1;
A4: dom ((((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) = (dom (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]))) \/ (dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) by FUNCT_4:def 1
.= ((dom ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).])) \/ (dom ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]))) \/ (dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) by FUNCT_4:def 1
.= ([.(a - c),(a + ((d - b) / (b / c))).] \/ (dom ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]))) \/ (dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) by FUNCT_2:def 1
.= ([.(a - c),(a + ((d - b) / (b / c))).] \/ [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) \/ (dom ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) by FUNCT_2:def 1
.= ([.(a - c),(a + ((d - b) / (b / c))).] \/ [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).]) \/ [.(a + ((b - d) / (b / c))),(a + c).] by FUNCT_2:def 1
.= [.(a - c),(a + ((b - d) / (b / c))).] \/ [.(a + ((b - d) / (b / c))),(a + c).] by XXREAL_1:165, A5, A6
.= [.(a - c),(a + c).] by XXREAL_1:165, A7, A8
.= dom (f | [.(a - c),(a + c).]) by FUNCT_2:def 1 ;
for x being object st x in dom (f | [.(a - c),(a + c).]) holds
(f | [.(a - c),(a + c).]) . x = ((((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) . x

proof

let x be object ; :: thesis: ( x in dom (f | [.(a - c),(a + c).]) implies (f | [.(a - c),(a + c).]) . x = ((((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) . x )
assume B0: x in dom (f | [.(a - c),(a + c).]) ; :: thesis: (f | [.(a - c),(a + c).]) . x = ((((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) . x
reconsider x = x as Real by B0;
set a1 = a + ((d - b) / (b / c));
set a2 = a + ((b - d) / (b / c));
(a + c) - (a + ((b - d) / (b / c))) = (- ((b - d) / (b / c))) + c
.= ((- (b - d)) / (b / c)) + c by XCMPLX_1:187 ;
then B1: ((a + ((d - b) / (b / c))) + c) - a = (a + c) - (a + ((b - d) / (b / c))) ;
B21: (- c) + c < ((d - b) / (b / c)) + c by XREAL_1:8, A5a;
then B2: ((a + ((d - b) / (b / c))) + c) - a > 0 ;
set c0 = ((a + ((d - b) / (b / c))) + c) - a;
B5: (a + ((d - b) / (b / c))) + (- (((a + ((d - b) / (b / c))) + c) - a)) < (a + ((b - d) / (b / c))) + (((a + ((d - b) / (b / c))) + c) - a) by A6, XREAL_1:8, B2;
B6: d / (((a + ((d - b) / (b / c))) + c) - a) = d / (((d - b) / (b / c)) + c)
.= d / (((d - b) + ((b / c) * c)) / (b / c)) by XCMPLX_1:113, A1
.= d / (((d - b) + b) / (b / c)) by XCMPLX_1:87, A1
.= b / c by XCMPLX_1:54, A1 ;
then B7: - ((d / (((a + ((d - b) / (b / c))) + c) - a)) * ((a + ((d - b) / (b / c))) - (((a + ((d - b) / (b / c))) + c) - a))) = (- ((b / c) * a)) + ((b / c) * c)
.= (- ((b / c) * a)) + b by A1, XCMPLX_1:87
.= b - (a * (b / c))
.= b - ((a * b) / c) by XCMPLX_1:74 ;
B8: (d / (((a + ((d - b) / (b / c))) + c) - a)) * ((a + ((b - d) / (b / c))) + (((a + ((d - b) / (b / c))) + c) - a)) = (b / c) * (((((- (d - b)) / (b / c)) + a) + ((d - b) / (b / c))) + c) by B6
.= (b / c) * ((((- ((d - b) / (b / c))) + a) + ((d - b) / (b / c))) + c) by XCMPLX_1:187
.= (a * (b / c)) + (c * (b / c))
.= (a * (b / c)) + b by A1, XCMPLX_1:87
.= b + ((a * b) / c) by XCMPLX_1:74 ;
(f | [.(a - c),(a + c).]) . x = f . x by FUNCT_1:49, B0
.= min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by A3
.= (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x by A1, A2, LmCri2
.= ((d (#) (TrapezoidalFS (((a + ((d - b) / (b / c))) - (((a + ((d - b) / (b / c))) + c) - a)),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),((a + ((b - d) / (b / c))) + (((a + ((d - b) / (b / c))) + c) - a))))) | [.((a + ((d - b) / (b / c))) - (((a + ((d - b) / (b / c))) + c) - a)),((a + ((b - d) / (b / c))) + (((a + ((d - b) / (b / c))) + c) - a)).]) . x by FUNCT_1:49, B0, B1
.= ((d (#) (TrapezoidalFS (((a + ((d - b) / (b / c))) - (((a + ((d - b) / (b / c))) + c) - a)),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),((a + ((b - d) / (b / c))) + (((a + ((d - b) / (b / c))) + c) - a))))) | ['((a + ((d - b) / (b / c))) - (((a + ((d - b) / (b / c))) + c) - a)),((a + ((b - d) / (b / c))) + (((a + ((d - b) / (b / c))) + c) - a))']) . x by INTEGRA5:def 3, B5
.= ((((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) . x by B6, FUZZY_7:47, B21, A1, A6, B1, B7, B8 ;
hence (f | [.(a - c),(a + c).]) . x = ((((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])) . x ; :: thesis: verum

end;

hence f | [.(a - c),(a + c).] = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).]) by A4, FUNCT_1:2; :: thesis: verum