k1: a + 0 < b by Z1;
k3: b < d by Z2, Z3, XXREAL_0:2;
set f1 = (AffineMap (0,0)) | (REAL \ ].a,d.[);
set f2 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f3 = (AffineMap (0,1)) | [.b,c.];
set f4 = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
set f = ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]);
a < c by Z1, Z2, XXREAL_0:2;
then REAL \ ].a,d.[ <> {} by RealNon, Z3, XXREAL_0:2;
then L1: rng ((AffineMap (0,0)) | (REAL \ ].a,d.[)) = {0} by Andr1a;
L2: rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.0,1.] by k1, Hope1, XREAL_1:20;
b in [.b,c.] by Z2;
then L3: rng ((AffineMap (0,1)) | [.b,c.]) = {1} by Andr1a;
c + 0 < d by Z3;
then L4: rng ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = [.0,1.] by Hope2a, XREAL_1:20;
Ss: rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) c= (rng ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_4:17;
rng ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) c= (rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (rng ((AffineMap (0,1)) | [.b,c.])) by FUNCT_4:17;
then d6: (rng ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.]))) \/ (rng ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) c= ((rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (rng ((AffineMap (0,1)) | [.b,c.]))) \/ (rng ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by XBOOLE_1:13;
rng (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) c= (rng ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.]))) \/ (rng ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by FUNCT_4:17;
then l6: rng (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) c= ((rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (rng ((AffineMap (0,1)) | [.b,c.]))) \/ (rng ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by d6;
[.0,0.] c= [.0,1.] by XXREAL_1:34;
then Hh: {0} c= [.0,1.] by XXREAL_1:17;
[.1,1.] c= [.0,1.] by XXREAL_1:34;
then {1} c= [.0,1.] by XXREAL_1:17;
then hx: {1} \/ [.0,1.] = [.0,1.] by XBOOLE_1:12;
ss: rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) c= [.0,1.] by Hh, Ss, L1, L2, XBOOLE_1:12;
sk: rng (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) c= (rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ [.0,1.] by hx, L3, XBOOLE_1:4, L4, l6;
(rng (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ [.0,1.] c= [.0,1.] \/ [.0,1.] by ss, XBOOLE_1:13;
then I3: rng (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) c= [.0,1.] by sk;
I5: dom (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = (dom ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by FUNCT_4:def 1
.= ((dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by FUNCT_4:def 1
.= (((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by FUNCT_4:def 1 ;
REAL \ ].a,d.[ c= REAL ;
then i7: REAL \ ].a,d.[ c= dom (AffineMap (0,0)) by FUNCT_2:def 1;
O4: ( a < +infty & c < +infty & d < +infty ) by XXREAL_0:9, XREAL_0:def 1;
a < c by Z1, Z2, XXREAL_0:2;
then O6: a < d by Z3, XXREAL_0:2;
O5: -infty < a by XXREAL_0:12, XREAL_0:def 1;
[.a,b.] c= REAL ;
then O1: [.a,b.] c= dom (AffineMap ((1 / (b - a)),(- (a / (b - a))))) by FUNCT_2:def 1;
[.b,c.] c= REAL ;
then j1: [.b,c.] c= dom (AffineMap (0,1)) by FUNCT_2:def 1;
[.c,d.] c= REAL ;
then OO: [.c,d.] c= dom (AffineMap ((- (1 / (d - c))),(d / (d - c)))) by FUNCT_2:def 1;
d2: (dom ((AffineMap (0,1)) | [.b,c.])) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = [.b,c.] \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by j1, RELAT_1:62
.= [.b,c.] \/ [.c,d.] by RELAT_1:62, OO
.= [.b,d.] by XXREAL_1:165, Z2, Z3 ;
d3: ((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ ((dom ((AffineMap (0,1)) | [.b,c.])) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by XBOOLE_1:4
.= [.a,b.] \/ [.b,d.] by d2, O1, RELAT_1:62
.= [.a,d.] by XXREAL_1:165, k3, Z1 ;
((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ ((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap (0,1)) | [.b,c.])))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = (dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by XBOOLE_1:4
.= (REAL \ ].a,d.[) \/ [.a,d.] by d3, i7, RELAT_1:62
.= (].-infty,a.] \/ [.d,+infty.[) \/ [.a,d.] by XXREAL_1:398
.= ].-infty,a.] \/ ([.d,+infty.[ \/ [.a,d.]) by XBOOLE_1:4
.= ].-infty,a.] \/ [.a,+infty.[ by XXREAL_1:176, O4, O6
.= ].-infty,+infty.[ by XXREAL_1:172, O4, O5 ;
then (((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = REAL by XBOOLE_1:4, XXREAL_1:224;
hence ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) is FuzzySet of REAL by FUNCT_2:2, I5, I3; :: thesis: verum