let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies for x being object st x in [.b,c.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap (0,1)) . x )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: for x being object st x in [.b,c.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap (0,1)) . x
then AA: d - c <> 0 ;
A11: ( a < c & b < d ) by A1, XXREAL_0:2;
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 [.b,c.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap (0,1)) . x

proof

let x be object ; :: thesis: ( x in [.b,c.] implies (TrapezoidalFS (a,b,c,d)) . x = (AffineMap (0,1)) . x )
assume A2: x in [.b,c.] ; :: thesis: (TrapezoidalFS (a,b,c,d)) . x = (AffineMap (0,1)) . x
then reconsider x = x as Real ;
TT: for x being object st x in (dom ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.]))) /\ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) holds
((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . 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.])) +* ((AffineMap (0,1)) | [.b,c.]))) /\ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) implies ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x )
assume B1: x in (dom ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.]))) /\ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x
then reconsider x = x as Real ;
x in (dom ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.]))) /\ [.c,d.] by B1, FUNCT_2:def 1;
then x in ((dom (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) /\ [.c,d.] by FUNCT_4:def 1;
then x in (((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) /\ [.c,d.] by FUNCT_4:def 1;
then x in (((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ [.c,d.]) \/ ((dom ((AffineMap (0,1)) | [.b,c.])) /\ [.c,d.]) by XBOOLE_1:23;
then x in (((dom ((AffineMap (0,0)) | (REAL \ ].a,d.[))) /\ [.c,d.]) \/ ((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) /\ [.c,d.])) \/ ((dom ((AffineMap (0,1)) | [.b,c.])) /\ [.c,d.]) by XBOOLE_1:23;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ ((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) /\ [.c,d.])) \/ ((dom ((AffineMap (0,1)) | [.b,c.])) /\ [.c,d.]) by FUNCT_2:def 1;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ ([.a,b.] /\ [.c,d.])) \/ ((dom ((AffineMap (0,1)) | [.b,c.])) /\ [.c,d.]) by FUNCT_2:def 1;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ ([.a,b.] /\ [.c,d.])) \/ ([.b,c.] /\ [.c,d.]) by FUNCT_2:def 1;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ ([.a,b.] /\ [.c,d.])) \/ [.(max (b,c)),(min (c,d)).] by XXREAL_1:140;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.(max (a,c)),(min (b,d)).]) \/ [.(max (b,c)),(min (c,d)).] by XXREAL_1:140;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.(max (a,c)),(min (b,d)).]) \/ [.c,(min (c,d)).] by XXREAL_0:def 10, A1;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.c,(min (b,d)).]) \/ [.c,(min (c,d)).] by XXREAL_0:def 10, A1, XXREAL_0:2;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.c,(min (b,d)).]) \/ [.c,c.] by XXREAL_0:def 9, A1;
then x in (((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.c,b.]) \/ [.c,c.] by XXREAL_0:def 9, A1, XXREAL_0:2;
then x in (((].-infty,a.] \/ [.d,+infty.[) /\ [.c,d.]) \/ [.c,b.]) \/ [.c,c.] by XXREAL_1:398;
then x in (((].-infty,a.] /\ [.c,d.]) \/ ([.d,+infty.[ /\ [.c,d.])) \/ [.c,b.]) \/ [.c,c.] by XBOOLE_1:23;
then x in (((].-infty,a.] /\ [.c,d.]) \/ ([.d,+infty.[ /\ [.c,d.])) \/ {}) \/ [.c,c.] by XXREAL_1:29, A1;
then ( x in (].-infty,a.] /\ [.c,d.]) \/ ([.d,+infty.[ /\ [.c,d.]) or x in [.c,c.] ) by XBOOLE_0:def 3;
then ( x in {} \/ ([.d,+infty.[ /\ [.c,d.]) or x in [.c,c.] ) by XBOOLE_0:def 7, XXREAL_1:280, A11;
then ( ( x in [.d,+infty.[ & x in [.c,d.] ) or x in [.c,c.] ) by XBOOLE_0:def 4;
then ( ( d <= x & x < +infty & c <= x & x <= d ) or x in [.c,c.] ) by XXREAL_1:1, XXREAL_1:3;

per cases then ( x in [.d,d.] or x in [.c,c.] ) ;

suppose x in [.d,d.] ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x

then D2s: x in {d} by XXREAL_1:17;
D3: not d in dom ((AffineMap (0,1)) | [.b,c.]) by XXREAL_1:1, A1;
D4: not d in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by XXREAL_1:1, A11;
D6: d in [.c,d.] by A1;
DD: ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . d by D2s, TARSKI:def 1
.= (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . d by FUNCT_4:11, D3
.= ((AffineMap (0,0)) | (REAL \ ].a,d.[)) . d by FUNCT_4:11, D4
.= (AffineMap (0,0)) . d by FUNCT_1:49, Th3
.= (0 * d) + 0 by FCONT_1:def 4 ;
((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . d by D2s, TARSKI:def 1
.= (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . d by FUNCT_1:49, D6
.= ((- (1 / (d - c))) * d) + (d / (d - c)) by FCONT_1:def 4
.= (- (d * (1 / (d - c)))) + (d / (d - c))
.= (- ((d * 1) / (d - c))) + (d / (d - c)) by XCMPLX_1:74
.= 0 ;
hence ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x by DD; :: thesis: verum

end;

suppose x in [.c,c.] ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x

then C2s: x in {c} by XXREAL_1:17;
C4: c in [.b,c.] by A1;
then C3: c in dom ((AffineMap (0,1)) | [.b,c.]) by FUNCT_2:def 1;
C5: c in [.c,d.] by A1;
CC: ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . c by C2s, TARSKI:def 1
.= ((AffineMap (0,1)) | [.b,c.]) . c by FUNCT_4:13, C3
.= (AffineMap (0,1)) . c by FUNCT_1:49, C4
.= (0 * c) + 1 by FCONT_1:def 4
.= 1 ;
((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . c by C2s, TARSKI:def 1
.= (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . c by C5, FUNCT_1:49
.= ((- (1 / (d - c))) * c) + (d / (d - c)) by FCONT_1:def 4
.= ((d * 1) / (d - c)) + (- (c * (1 / (d - c))))
.= (d * (1 / (d - c))) + (- (c * (1 / (d - c)))) by XCMPLX_1:74
.= (d - c) * (1 / (d - c))
.= ((d - c) * 1) / (d - c) by XCMPLX_1:74
.= 1 by AA, XCMPLX_1:60 ;
hence ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . x = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x by CC; :: thesis: verum

end;

end;

end;

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

end;

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