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

proof

let x be Real; :: thesis: ( not x in [.a,d.] implies (TrapezoidalFS (a,b,c,d)) . x = 0 )
assume not x in [.a,d.] ; :: thesis: (TrapezoidalFS (a,b,c,d)) . x = 0

per cases then ( x < a or d < x ) ;

suppose B1: x < a ; :: thesis: (TrapezoidalFS (a,b,c,d)) . x = 0

then x < c by XXREAL_0:2, AA;
then A4: not x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by XXREAL_1:1;
x < b by A1, B1, XXREAL_0:2;
then A5: not x in dom ((AffineMap (0,1)) | [.b,c.]) by XXREAL_1:1;
A6: not x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by B1, XXREAL_1:1;
-infty < x by XXREAL_0:12, XREAL_0:def 1;
then ( x in ].-infty,a.] or x in [.d,+infty.[ ) by B1;
then x in ].-infty,a.] \/ [.d,+infty.[ by XBOOLE_0:def 3;
then A7: x in REAL \ ].a,d.[ by XXREAL_1:398;
(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, A4
.= (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x by FUNCT_4:11, A5
.= ((AffineMap (0,0)) | (REAL \ ].a,d.[)) . x by FUNCT_4:11, A6
.= (AffineMap (0,0)) . x by FUNCT_1:49, A7
.= (0 * x) + 0 by FCONT_1:def 4 ;
hence (TrapezoidalFS (a,b,c,d)) . x = 0 ; :: thesis: verum

end;

suppose C1: d < x ; :: thesis: (TrapezoidalFS (a,b,c,d)) . x = 0

then A4: not x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by XXREAL_1:1;
c < x by A1, C1, XXREAL_0:2;
then A5: not x in dom ((AffineMap (0,1)) | [.b,c.]) by XXREAL_1:1;
b < x by XXREAL_0:2, AA, C1;
then A6: not x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by XXREAL_1:1;
x < +infty by XXREAL_0:9, XREAL_0:def 1;
then ( x in ].-infty,a.] or x in [.d,+infty.[ ) by C1;
then x in ].-infty,a.] \/ [.d,+infty.[ by XBOOLE_0:def 3;
then A7: x in REAL \ ].a,d.[ by XXREAL_1:398;
(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, A4
.= (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x by FUNCT_4:11, A5
.= ((AffineMap (0,0)) | (REAL \ ].a,d.[)) . x by FUNCT_4:11, A6
.= (AffineMap (0,0)) . x by FUNCT_1:49, A7
.= (0 * x) + 0 by FCONT_1:def 4 ;
hence (TrapezoidalFS (a,b,c,d)) . x = 0 ; :: thesis: verum

end;

end;

end;

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