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

proof

let x be object ; :: thesis: ( x in [.c,d.] implies (TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . x )
assume A2: x in [.c,d.] ; :: thesis: (TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . x
then A3: x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by FUNCT_2:def 1;
thus (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 ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x by FUNCT_4:13, A3
.= (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . x by A2, FUNCT_1:49 ; :: thesis: verum

end;

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