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; verum