let a, b, c, d, r, s, x be Real; :: thesis: ( a < b & b < c & c < d & r >= 0 & s >= 0 & x in [.a,d.] implies ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0 )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: ( not r >= 0 or not s >= 0 or not x in [.a,d.] or ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0 )
assume A2: ( r >= 0 & s >= 0 ) ; :: thesis: ( not x in [.a,d.] or ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0 )
assume A3: x in [.a,d.] ; :: thesis: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0

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

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

A42: x <= d by XXREAL_1:1, A3;
x in [.c,+infty.[ by A4, XXREAL_1:236;
then A41: x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) by FUNCT_2:def 1;
then A43: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x = ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) . x by FUNCT_4:13
.= (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . x by FUNCT_1:47, A41
.= (((- s) / (d - c)) * x) + (- ((d * (- s)) / (d - c))) by FCONT_1:def 4
.= (((- s) / (d - c)) * x) + ((- (d * (- s))) / (d - c)) by XCMPLX_1:187
.= (((- s) / (d - c)) * x) + (((- d) * (- s)) / (d - c))
.= (((- s) / (d - c)) * x) + (((- s) / (d - c)) * (- d)) by XCMPLX_1:74
.= ((- s) / (d - c)) * (x - d) ;
B1: ( 0 < d - c & - s <= 0 ) by A2, A1, XREAL_1:50;
x - d <= 0 by A42, XREAL_1:47;
hence ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0 by A43, B1; :: thesis: verum

end;

suppose A5: x < c ; :: thesis: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0

then A51: not x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) by XXREAL_1:236;

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

suppose A6: b <= x ; :: thesis: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0

then x in [.b,c.] by A5;
then A61: x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) by FUNCT_2:def 1;
A65: c - b <> 0 by A1;
A64: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x by A51, FUNCT_4:11
.= ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) . x by A61, FUNCT_4:13
.= (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . x by FUNCT_1:47, A61
.= (((s - r) / (c - b)) * x) + (s - ((c * (s - r)) / (c - b))) by FCONT_1:def 4
.= ((x * (s - r)) / (c - b)) + (s - ((c * (s - r)) / (c - b))) by XCMPLX_1:74
.= (((x * (s - r)) / (c - b)) + s) - ((c * (s - r)) / (c - b))
.= (((x * (s - r)) / (c - b)) + ((s * (c - b)) / (c - b))) - ((c * (s - r)) / (c - b)) by XCMPLX_1:89, A65
.= (((x * (s - r)) / (c - b)) + ((s * (c - b)) / (c - b))) + (- ((c * (s - r)) / (c - b)))
.= (((x * (s - r)) / (c - b)) + ((s * (c - b)) / (c - b))) + ((- (c * (s - r))) / (c - b)) by XCMPLX_1:187
.= (((x * (s - r)) + (s * (c - b))) + ((- c) * (s - r))) / (c - b) by XCMPLX_1:63
.= ((s * (x - b)) + (r * (c - x))) / (c - b) ;
A62: x - b >= 0 by A6, XREAL_1:48;
A63: c - x > 0 by A5, XREAL_1:50;
c - b > 0 by XREAL_1:50, A1;
hence ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0 by A64, A63, A62, A2; :: thesis: verum

end;

suppose A7: x < b ; :: thesis: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0

then A72: not x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) by XXREAL_1:1;
x < c by A1, A7, XXREAL_0:2;
then A74: not x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) by XXREAL_1:236;
x in ].-infty,b.] by A7, XXREAL_1:234;
then A71: x in dom ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) by FUNCT_2:def 1;
A73: ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x by A74, FUNCT_4:11
.= ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) . x by A72, FUNCT_4:11
.= (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . x by A71, FUNCT_1:47
.= ((r / (b - a)) * x) + (- ((a * r) / (b - a))) by FCONT_1:def 4
.= ((r / (b - a)) * x) + ((- (a * r)) / (b - a)) by XCMPLX_1:187
.= ((r / (b - a)) * x) + (((- a) * r) / (b - a))
.= ((r / (b - a)) * x) + ((r / (b - a)) * (- a)) by XCMPLX_1:74
.= (r / (b - a)) * (x + (- a)) ;
a <= x by A3, XXREAL_1:1;
then A72: 0 <= x - a by XREAL_1:48;
b - a > 0 by XREAL_1:50, A1;
hence ((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0 by A73, A72, A2; :: thesis: verum

end;

end;

end;

end;