let a, b, c be Real; ( a < b & b < c implies TriangularFS (a,b,c) is continuous )
assume that
Z1:
a < b
and
Z2:
b < c
; 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 ;
( x in (dom g) /\ (dom h) implies g . x = h . x )
assume
x in (dom g) /\ (dom h)
;
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
;
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; verum