let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies TrapezoidalFS (a,b,c,d) is continuous )
assume that
Z1: a < b and
Z2: b < c and
Z3: c < d ; :: thesis: TrapezoidalFS (a,b,c,d) is continuous
set F = TrapezoidalFS (a,b,c,d);
S1: TrapezoidalFS (a,b,c,d) = ((((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.]) by Z1, Z2, Z3, TPDef;
set f1 = AffineMap (0,0);
set f = (AffineMap (0,0)) | (REAL \ ].a,d.[);
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 / (d - c))),(d / (d - c)));
reconsider h = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.] as PartFunc of REAL,REAL ;
set i1 = AffineMap (0,1);
reconsider i = (AffineMap (0,1)) | [.b,c.] as PartFunc of REAL,REAL ;
[.a,b.] c= REAL ;
then d9: [.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;
[.c,d.] c= REAL ;
then d3: [.c,d.] c= dom (AffineMap ((- (1 / (d - c))),(d / (d - c)))) by FUNCT_2:def 1;
then J3: dom h = [.c,d.] by RELAT_1:62;
[.b,c.] c= REAL ;
then d8: [.b,c.] c= dom (AffineMap (0,1)) by FUNCT_2:def 1;
then JW: dom i = [.b,c.] by RELAT_1:62;
b in dom g by J2, Z1;
then j2: not g is empty ;
c in dom h by J3, Z3;
then j3: not h is empty ;
ff: for x being object st x in (dom g) /\ (dom i) holds
g . x = i . x

proof

let x be object ; :: thesis: ( x in (dom g) /\ (dom i) implies g . x = i . x )
assume x in (dom g) /\ (dom i) ; :: thesis: g . x = i . x
then i1: x in {b} by XXREAL_1:418, Z1, Z2, J2, JW;
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;
i . x = i . b by i1, TARSKI:def 1
.= (AffineMap (0,1)) . b by FUNCT_1:49, II
.= 1 by Kici1
.= (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 = i . x ; :: thesis: verum

end;

set gh = g +* i;
z1: dom (g +* i) = (dom g) \/ (dom i) by FUNCT_4:def 1
.= [.a,b.] \/ [.b,c.] by d9, RELAT_1:62, JW
.= [.a,c.] by XXREAL_1:165, Z1, Z2 ;
V5: a < c by XXREAL_0:2, Z1, Z2;
then PS: a in dom (g +* i) by z1;
then reconsider gh = g +* i as non empty PartFunc of REAL,REAL ;
K2: a in [.a,b.] by Z1;
then W3: gh . 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 ;
P3: c in [.b,c.] by Z2;
K1: c in [.c,d.] by Z3;
N3: dom h = [.c,d.] by d3, RELAT_1:62;
c + 0 < d by Z3;
then MN: d - c > 0 by XREAL_1:20;
N4: h . c = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . c by FUNCT_1:49, K1
.= 1 by Cb1, MN ;
KK: d in [.c,d.] by Z3;
then N5: h . d = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . d by FUNCT_1:49
.= 0 by Cb2 ;
NN: gh is continuous by Glue, ff, j2, J2, JW, d8, P3, PARTFUN1:def 4;
M1: for x being object st x in (dom gh) /\ (dom h) holds
gh . x = h . x

proof

let x be object ; :: thesis: ( x in (dom gh) /\ (dom h) implies gh . x = h . x )
assume x in (dom gh) /\ (dom h) ; :: thesis: gh . x = h . x
then ll: x in {c} by XXREAL_1:418, Z3, V5, J3, z1;
then gh . x = gh . c by TARSKI:def 1
.= i . c by FUNCT_4:13, P3, JW
.= (AffineMap (0,1)) . c by FUNCT_1:49, P3
.= h . c by N4, Kici1
.= h . x by ll, TARSKI:def 1 ;
hence gh . x = h . x ; :: thesis: verum

end;

then fG: gh tolerates h by PARTFUN1:def 4;
set ghi = gh +* h;
V3: dom (gh +* h) = (dom gh) \/ (dom h) by FUNCT_4:def 1
.= [.a,c.] \/ [.c,d.] by z1, d3, RELAT_1:62
.= [.a,d.] by XXREAL_1:165, Z3, V5 ;
V4: (gh +* h) . a = 0 by FUNCT_4:15, M1, PARTFUN1:def 4, PS, W3;
(gh +* h) . d = 0 by N3, FUNCT_4:13, KK, N5;
then consider hh being PartFunc of REAL,REAL such that
TT: ( hh = ((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* (gh +* h) & ( for x being Real st x in dom hh holds
hh is_continuous_in x ) ) by Kluczyk, V3, V4, Glue, NN, j3, z1, J3, fG;
hh = (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* (g +* i)) +* h by FUNCT_4:14, TT
.= ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* g) +* i) +* h by FUNCT_4:14 ;
hence TrapezoidalFS (a,b,c,d) is continuous by TT, S1; :: thesis: verum