let p, q, s, t be Real; :: thesis: for f being Function of REAL,REAL st p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 & ( for x being Real holds f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x ) holds
max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))
let f be Function of REAL,REAL; :: thesis: ( p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 & ( for x being Real holds f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x ) implies max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) )
assume A1: ( p * s < 0 & p > 0 ) ; :: thesis: ( not ((p * t) - (q * s)) / (p - s) > 0 or ex x being Real st not f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x or max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) )
assume A2: ((p * t) - (q * s)) / (p - s) > 0 ; :: thesis: ( ex x being Real st not f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x or max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) )
assume A3: for x being Real holds f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x ; :: thesis: max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))
set r = ((p * t) - (q * s)) / (p - s);
dom (max+ f) = dom f by RFUNCT_3:def 10
.= REAL by FUNCT_2:def 1 ;
then A4: dom (max+ f) = dom ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) by FUNCT_2:def 1;
A9: s < 0 by A1;
for x being object st x in dom (max+ f) holds
(max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x

proof

let x be object ; :: thesis: ( x in dom (max+ f) implies (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x )
assume A5: x in dom (max+ f) ; :: thesis: (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x
then reconsider x = x as Real ;
A6: (max+ f) . x = max+ (f . x) by RFUNCT_3:def 10, A5
.= max ((f . x),0) by RFUNCT_3:def 1 ;
set a = - (q / p);
set b = (t - q) / (p - s);
set c = - (t / s);
A7: ( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) ) by Th13, A1, A2;

per cases ( x in ].(- (q / p)),(- (t / s)).[ or not x in ].(- (q / p)),(- (t / s)).[ ) ;

suppose x in ].(- (q / p)),(- (t / s)).[ ; :: thesis: (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x

then B2: ( - (q / p) <= x & x <= - (t / s) ) by XXREAL_1:4;

per cases ( x < (t - q) / (p - s) or (t - q) / (p - s) <= x ) ;

suppose B5: x < (t - q) / (p - s) ; :: thesis: (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x

then B6: not x in dom ((AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))) | [.((t - q) / (p - s)),(- (t / s)).]) by XXREAL_1:1;
B4: x in [.(- (q / p)),((t - q) / (p - s)).] by B5, B2;
then B7: x in dom ((AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))))) | [.(- (q / p)),((t - q) / (p - s)).]) by FUNCT_2:def 1;
B8: not x in dom ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) by B5, XXREAL_1:236;
B11: f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x by A3
.= ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) . x by FUNCT_4:11, B8
.= (AffineMap (p,q)) . x by FUNCT_1:49, B5, XXREAL_1:234
.= (p * x) + q by FCONT_1:def 4 ;
(- (q / p)) * p <= x * p by B2, XREAL_1:64, A1;
then - ((q / p) * p) <= x * p ;
then - q <= x * p by XCMPLX_1:87, A1;
then B10: (- q) + q <= (x * p) + q by XREAL_1:6;
((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x = (((p * t) - (q * s)) / (p - s)) * ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) . x) by VALUED_1:6
.= (((p * t) - (q * s)) / (p - s)) * (((((AffineMap (0,0)) | (REAL \ ].(- (q / p)),(- (t / s)).[)) +* ((AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))))) | [.(- (q / p)),((t - q) / (p - s)).])) +* ((AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))) | [.((t - q) / (p - s)),(- (t / s)).])) . x) by FUZNUM_1:def 7, A7
.= (((p * t) - (q * s)) / (p - s)) * ((((AffineMap (0,0)) | (REAL \ ].(- (q / p)),(- (t / s)).[)) +* ((AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))))) | [.(- (q / p)),((t - q) / (p - s)).])) . x) by FUNCT_4:11, B6
.= (((p * t) - (q * s)) / (p - s)) * (((AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))))) | [.(- (q / p)),((t - q) / (p - s)).]) . x) by FUNCT_4:13, B7
.= (((p * t) - (q * s)) / (p - s)) * ((AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))))) . x) by FUNCT_1:49, B4
.= (((p * t) - (q * s)) / (p - s)) * (((1 / (((t - q) / (p - s)) - (- (q / p)))) * x) + (- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p)))))) by FCONT_1:def 4
.= (((((p * t) - (q * s)) / (p - s)) * (1 / (((t - q) / (p - s)) + (q / p)))) * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / (((t - q) / (p - s)) + (q / p)))))
.= (((((p * t) - (q * s)) / (p - s)) * (1 / ((1 / p) * (((p * t) - (q * s)) / (p - s))))) * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / (((t - q) / (p - s)) + (q / p))))) by A1, Th14
.= (((((p * t) - (q * s)) / (p - s)) * (1 / ((1 / p) * (((p * t) - (q * s)) / (p - s))))) * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / ((1 / p) * (((p * t) - (q * s)) / (p - s)))))) by A1, Th14
.= (((((p * t) - (q * s)) / (p - s)) * (1 / ((((p * t) - (q * s)) / (p - s)) / p))) * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / ((1 / p) * (((p * t) - (q * s)) / (p - s)))))) by XCMPLX_1:99
.= (((((p * t) - (q * s)) / (p - s)) * (p / (((p * t) - (q * s)) / (p - s)))) * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / ((1 / p) * (((p * t) - (q * s)) / (p - s)))))) by XCMPLX_1:57
.= (p * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / ((1 / p) * (((p * t) - (q * s)) / (p - s)))))) by XCMPLX_1:87, A2
.= (p * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / ((((p * t) - (q * s)) / (p - s)) / p)))) by XCMPLX_1:99
.= (p * x) + (- ((((p * t) - (q * s)) / (p - s)) * ((- (q / p)) / ((((p * t) - (q * s)) / (p - s)) / p))))
.= (p * x) + (- ((((p * t) - (q * s)) / (p - s)) * (- ((q / p) / ((((p * t) - (q * s)) / (p - s)) / p))))) by XCMPLX_1:187
.= (p * x) + ((((p * t) - (q * s)) / (p - s)) * ((q / p) / ((((p * t) - (q * s)) / (p - s)) / p)))
.= (p * x) + ((((p * t) - (q * s)) / (p - s)) * (q / (((p * t) - (q * s)) / (p - s)))) by XCMPLX_1:55, A1
.= (p * x) + q by XCMPLX_1:87, A2 ;
hence (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x by XXREAL_0:def 10, B10, B11, A6; :: thesis: verum

end;

suppose B51: (t - q) / (p - s) <= x ; :: thesis: (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x

then x in [.((t - q) / (p - s)),+infty.[ by XXREAL_1:236;
then B91: x in dom ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) by FUNCT_2:def 1;
x * s >= (- (t / s)) * s by B2, XREAL_1:65, A9;
then x * s >= - ((t / s) * s) ;
then x * s >= - t by XCMPLX_1:87, A9;
then B101s: (x * s) + t >= (- t) + t by XREAL_1:6;
B111: f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x by A3
.= ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) . x by FUNCT_4:13, B91
.= (AffineMap (s,t)) . x by FUNCT_1:49, B51, XXREAL_1:236
.= (s * x) + t by FCONT_1:def 4 ;
B41: x in [.((t - q) / (p - s)),(- (t / s)).] by B51, B2;
then B71: x in dom ((AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))) | [.((t - q) / (p - s)),(- (t / s)).]) by FUNCT_2:def 1;
((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x = (((p * t) - (q * s)) / (p - s)) * ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) . x) by VALUED_1:6
.= (((p * t) - (q * s)) / (p - s)) * (((((AffineMap (0,0)) | (REAL \ ].(- (q / p)),(- (t / s)).[)) +* ((AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))))) | [.(- (q / p)),((t - q) / (p - s)).])) +* ((AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))) | [.((t - q) / (p - s)),(- (t / s)).])) . x) by FUZNUM_1:def 7, A7
.= (((p * t) - (q * s)) / (p - s)) * (((AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))) | [.((t - q) / (p - s)),(- (t / s)).]) . x) by FUNCT_4:13, B71
.= (((p * t) - (q * s)) / (p - s)) * ((AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))) . x) by FUNCT_1:49, B41
.= (((p * t) - (q * s)) / (p - s)) * (((- (1 / ((- (t / s)) - ((t - q) / (p - s))))) * x) + ((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s))))) by FCONT_1:def 4
.= ((((p * t) - (q * s)) / (p - s)) * ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))) * x)) + ((((p * t) - (q * s)) / (p - s)) * ((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))))
.= (((((p * t) - (q * s)) / (p - s)) * (- (1 / (- ((t / s) + ((t - q) / (p - s))))))) * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((t / s) + ((t - q) / (p - s))))) by XCMPLX_1:74
.= (((((p * t) - (q * s)) / (p - s)) * (- (1 / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))))) * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((t / s) + ((t - q) / (p - s))))) by A1, Th14
.= (((((p * t) - (q * s)) / (p - s)) * (- (1 / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))))) * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))) by A1, Th14
.= (((((p * t) - (q * s)) / (p - s)) * (- (- (1 / ((1 / s) * (((p * t) - (q * s)) / (p - s))))))) * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))) by XCMPLX_1:188
.= (((((p * t) - (q * s)) / (p - s)) * (1 / ((((p * t) - (q * s)) / (p - s)) / s))) * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))) by XCMPLX_1:99
.= (((((p * t) - (q * s)) / (p - s)) * (s / (((p * t) - (q * s)) / (p - s)))) * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))) by XCMPLX_1:57
.= (s * x) + (((((p * t) - (q * s)) / (p - s)) * (- (t / s))) / (- ((1 / s) * (((p * t) - (q * s)) / (p - s))))) by XCMPLX_1:87, A2
.= (s * x) + ((((p * t) - (q * s)) / (p - s)) * ((- (t / s)) / (- ((1 / s) * (((p * t) - (q * s)) / (p - s)))))) by XCMPLX_1:74
.= (s * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (t / s)) / ((1 / s) * (((p * t) - (q * s)) / (p - s)))))) by XCMPLX_1:188
.= (s * x) + ((((p * t) - (q * s)) / (p - s)) * (- ((- (t / s)) / ((((p * t) - (q * s)) / (p - s)) / s)))) by XCMPLX_1:99
.= (s * x) + ((((p * t) - (q * s)) / (p - s)) * (- (- ((t / s) / ((((p * t) - (q * s)) / (p - s)) / s))))) by XCMPLX_1:187
.= (s * x) + ((((p * t) - (q * s)) / (p - s)) * (t / (((p * t) - (q * s)) / (p - s)))) by XCMPLX_1:55, A9
.= (s * x) + t by XCMPLX_1:87, A2 ;
hence (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x by XXREAL_0:def 10, B101s, B111, A6; :: thesis: verum

end;

end;

end;

suppose C1: not x in ].(- (q / p)),(- (t / s)).[ ; :: thesis: (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x

then (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0 by A1, A2, Th15;
then C2: f . x <= 0 by A3;
((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x = (((p * t) - (q * s)) / (p - s)) * ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) . x) by VALUED_1:6
.= (((p * t) - (q * s)) / (p - s)) * ((AffineMap (0,0)) . x) by FUZZY_8:48, C1, A7
.= (((p * t) - (q * s)) / (p - s)) * ((0 * x) + 0) by FCONT_1:def 4 ;
hence (max+ f) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x by XXREAL_0:def 10, C2, A6; :: thesis: verum

end;

end;

end;

hence max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) by FUNCT_1:2, A4; :: thesis: verum