let a, b, c, d, r, s, x be Real; :: thesis: ( a < b & b < c & c < d & r >= 0 & s >= 0 & ( x < a or d < x ) 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 < a & not d < x ) 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 < a & not d < x ) 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 ( x < a or d < 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

per cases then ( x < a or d < x ) ;

suppose A4: x < a ; :: 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 < b by A1, XXREAL_0:2;
then A42: not x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) by XXREAL_1:1;
a < c by A1, XXREAL_0:2;
then x < c by A4, XXREAL_0:2;
then A41: not x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) by XXREAL_1:236;
x in ].-infty,b.] by XXREAL_1:234, A4, A1, XXREAL_0:2;
then A43: x in dom ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) by FUNCT_2:def 1;
C2: ((((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 A41, FUNCT_4:11
.= ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) . x by A42, FUNCT_4:11
.= (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . x by A43, 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)) ;
C1: 0 < b - a by A1, XREAL_1:50;
x - a < 0 by A4, XREAL_1:49;
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 C2, C1, A2; :: thesis: verum

end;

suppose A5: d < 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 [.c,+infty.[ by XXREAL_1:236, A1, XXREAL_0:2;
then A51: x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) by FUNCT_2:def 1;
B2: ((((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 A51, FUNCT_4:13
.= (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . x by A51, FUNCT_1:47
.= (((- 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;
0 < x - d by A5, XREAL_1:50;
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 B2, B1; :: thesis: verum

end;

end;