k1: a + 0 < b by Z1;
k2: b + 0 < c by Z2;
set f1 = (AffineMap (0,0)) | (REAL \ ].a,c.[);
set f2 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f3 = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.];
set f = (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]);
REAL \ ].a,c.[ <> {} by RealNon, Z1, Z2, XXREAL_0:2;
then L1: rng ((AffineMap (0,0)) | (REAL \ ].a,c.[)) = {0} by Andr1a;
L2: rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.0,1.] by k1, Hope1, XREAL_1:20;
L3: rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.] by Hope2a, k2, XREAL_1:20;
rng (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) c= (rng ((AffineMap (0,0)) | (REAL \ ].a,c.[))) \/ (rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_4:17;
then L5: (rng (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) c= ({0} \/ [.0,1.]) \/ (rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by XBOOLE_1:13, L1, L2;
l6: rng ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) c= (rng (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_4:17;
[.0,0.] c= [.0,1.] by XXREAL_1:34;
then {0} c= [.0,1.] by XXREAL_1:17;
then {0} \/ [.0,1.] = [.0,1.] by XBOOLE_1:12;
then I3: rng ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) c= [.0,1.] by l6, L3, L5;
I5: dom ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) = (dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_4:def 1
.= ((dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_4:def 1 ;
REAL \ ].a,c.[ c= REAL ;
then i7: REAL \ ].a,c.[ c= dom (AffineMap (0,0)) by FUNCT_2:def 1;
O4: ( a < +infty & c < +infty ) by XXREAL_0:9, XREAL_0:def 1;
O3: a < c by Z1, Z2, 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 O2: [.b,c.] c= dom (AffineMap ((- (1 / (c - b))),(c / (c - b)))) by FUNCT_2:def 1;
(dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) = [.a,b.] \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by RELAT_1:62, O1
.= [.a,b.] \/ [.b,c.] by RELAT_1:62, O2
.= [.a,c.] by XXREAL_1:165, Z1, Z2 ;
then (dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) \/ ((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) = (REAL \ ].a,c.[) \/ [.a,c.] by i7, RELAT_1:62
.= (].-infty,a.] \/ [.c,+infty.[) \/ [.a,c.] by XXREAL_1:398
.= ].-infty,a.] \/ ([.c,+infty.[ \/ [.a,c.]) by XBOOLE_1:4
.= ].-infty,a.] \/ [.a,+infty.[ by XXREAL_1:176, O3, O4
.= ].-infty,+infty.[ by XXREAL_1:172, O4, O5 ;
then ((dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) = REAL by XBOOLE_1:4, XXREAL_1:224;
hence (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) is FuzzySet of REAL by FUNCT_2:2, I5, I3; :: thesis: verum