let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies for x being object st x in [.a,b.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: for x being object st x in [.a,b.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x
then AA: b - a <> 0 ;
set f0 = (AffineMap (0,0)) | (REAL \ ].a,d.[);
set fab = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set fbc = (AffineMap (0,1)) | [.b,c.];
set fcd = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
for x being object st x in [.a,b.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x

proof

let x be object ; :: thesis: ( x in [.a,b.] implies (TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x )
assume A3: x in [.a,b.] ; :: thesis: (TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x
then reconsider x = x as Real ;
( a <= x & x <= b ) by A3, XXREAL_1:1;
then x < c by A1, XXREAL_0:2;
then A2: not x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by XXREAL_1:1;
A4: for x being object st x in (dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap (0,1)) | [.b,c.])) holds
(((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap (0,1)) | [.b,c.]) . x

proof

let x be object ; :: thesis: ( x in (dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap (0,1)) | [.b,c.])) implies (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap (0,1)) | [.b,c.]) . x )
assume B1: x in (dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap (0,1)) | [.b,c.])) ; :: thesis: (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap (0,1)) | [.b,c.]) . x
then reconsider x = x as Real ;
B2s: (dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap (0,1)) | [.b,c.])) = ((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap (0,1)) | [.b,c.])) by FUNCT_4:def 1
.= ((REAL \ ].a,d.[) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap (0,1)) | [.b,c.])) by FUNCT_2:def 1
.= ((REAL \ ].a,d.[) \/ [.a,b.]) /\ (dom ((AffineMap (0,1)) | [.b,c.])) by FUNCT_2:def 1
.= ((REAL \ ].a,d.[) \/ [.a,b.]) /\ [.b,c.] by FUNCT_2:def 1
.= ((REAL \ ].a,d.[) /\ [.b,c.]) \/ ([.a,b.] /\ [.b,c.]) by XBOOLE_1:23
.= {} \/ ([.a,b.] /\ [.b,c.]) by Th5, A1
.= [.(max (a,b)),(min (b,c)).] by XXREAL_1:140
.= [.b,(min (b,c)).] by XXREAL_0:def 10, A1
.= [.b,b.] by XXREAL_0:def 9, A1
.= {b} by XXREAL_1:17 ;
B3: b in [.b,c.] by A1;
B4: b in [.a,b.] by A1;
then B6: b in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by FUNCT_2:def 1;
B5: (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . b by B2s, B1, TARSKI:def 1
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . b by FUNCT_4:13, B6
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b by FUNCT_1:49, B4
.= (b * (1 / (b - a))) + (- ((a * 1) / (b - a))) by FCONT_1:def 4
.= (b * (1 / (b - a))) + (- (a * (1 / (b - a)))) by XCMPLX_1:74
.= (b - a) * (1 / (b - a))
.= ((b - a) * 1) / (b - a) by XCMPLX_1:74
.= 1 by AA, XCMPLX_1:60 ;
((AffineMap (0,1)) | [.b,c.]) . x = ((AffineMap (0,1)) | [.b,c.]) . b by B2s, B1, TARSKI:def 1
.= (AffineMap (0,1)) . b by FUNCT_1:49, B3
.= (0 * b) + 1 by FCONT_1:def 4 ;
hence (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap (0,1)) | [.b,c.]) . x by B5; :: thesis: verum

end;

x in (REAL \ ].a,d.[) \/ [.a,b.] by XBOOLE_0:def 3, A3;
then x in (REAL \ ].a,d.[) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_2:def 1;
then x in (dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_2:def 1;
then A5: x in dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_4:def 1;
A6: x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by A3, FUNCT_2:def 1;
(TrapezoidalFS (a,b,c,d)) . x = (((((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.])) . x by FUZNUM_1:def 8, A1
.= ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x by FUNCT_4:11, A2
.= (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x by FUNCT_4:15, A4, A5, PARTFUN1:def 4
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . x by FUNCT_4:13, A6 ;
hence (TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x by FUNCT_1:49, A3; :: thesis: verum

end;

hence for x being object st x in [.a,b.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x ; :: thesis: verum