let a, b, c be Real; :: thesis: ( a < b & b < c implies TriangularFS (a,b,c) is continuous )
assume that
Z1: a < b and
Z2: b < c ; :: thesis: TriangularFS (a,b,c) is continuous
set F = TriangularFS (a,b,c);
S1: TriangularFS (a,b,c) = (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by Z1, Z2, TrDef;
set f1 = AffineMap (0,0);
set f = (AffineMap (0,0)) | (REAL \ ].a,c.[);
set g1 = AffineMap ((1 / (b - a)),(- (a / (b - a))));
reconsider g = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.] as PartFunc of REAL,REAL ;
set h1 = AffineMap ((- (1 / (c - b))),(c / (c - b)));
reconsider h = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.] as PartFunc of REAL,REAL ;
[.a,b.] c= REAL ;
then [.a,b.] c= dom (AffineMap ((1 / (b - a)),(- (a / (b - a))))) by FUNCT_2:def 1;
then J2: dom g = [.a,b.] by RELAT_1:62;
[.b,c.] c= REAL ;
then h1: [.b,c.] c= dom (AffineMap ((- (1 / (c - b))),(c / (c - b)))) by FUNCT_2:def 1;
then J3: dom h = [.b,c.] by RELAT_1:62;
b in dom g by J2, Z1;
then j2: not g is empty ;
b in dom h by J3, Z2;
then j3: not h is empty ;
ff: for x being object st x in (dom g) /\ (dom h) holds
g . x = h . x

proof

let x be object ; :: thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x )
assume x in (dom g) /\ (dom h) ; :: thesis: g . x = h . x
then i1: x in {b} by XXREAL_1:418, Z1, Z2, J2, J3;
II: ( b in [.a,b.] & b in [.b,c.] ) by Z1, Z2;
a + 0 < b by Z1;
then I0: b - a > 0 by XREAL_1:20;
b + 0 < c by Z2;
then I2: c - b > 0 by XREAL_1:20;
h . x = h . b by i1, TARSKI:def 1
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b by FUNCT_1:49, II
.= 1 by Cb1, I2
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b by I0, Ab1
.= g . b by FUNCT_1:49, II
.= g . x by i1, TARSKI:def 1 ;
hence g . x = h . x ; :: thesis: verum

end;

then fF: g tolerates h by PARTFUN1:def 4;
set gh = g +* h;
z1: dom (g +* h) = (dom g) \/ (dom h) by FUNCT_4:def 1
.= [.a,b.] \/ [.b,c.] by J2, h1, RELAT_1:62
.= [.a,c.] by XXREAL_1:165, Z1, Z2 ;
K2: a in [.a,b.] by Z1;
then W3: (g +* h) . a = g . a by FUNCT_4:15, PARTFUN1:def 4, ff, J2
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a by FUNCT_1:49, K2
.= 0 by Ah1 ;
K1: c in [.b,c.] by Z2;
c in dom h by J3, Z2;
then (g +* h) . c = h . c by FUNCT_4:13
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c by K1, FUNCT_1:49
.= 0 by Cb2 ;
then consider hh being PartFunc of REAL,REAL such that
TT: ( hh = ((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* (g +* h) & ( for x being Real st x in dom hh holds
hh is_continuous_in x ) ) by W3, Kluczyk, fF, z1, Glue, J2, j2, j3, J3;
hh = TriangularFS (a,b,c) by TT, FUNCT_4:14, S1;
hence TriangularFS (a,b,c) is continuous by TT; :: thesis: verum