let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies TrapezoidalFS (a,b,c,d) is normalized )
set F = TrapezoidalFS (a,b,c,d);
reconsider bb = c as Element of REAL by XREAL_0:def 1;
assume Z1: ( a < b & b < c & c < d ) ; :: thesis: TrapezoidalFS (a,b,c,d) is normalized
s0: bb in [.c,d.] by Z1;
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, TPDef;
s2: dom (AffineMap ((- (1 / (d - c))),(d / (d - c)))) = REAL by FUNCT_2:def 1;
c + 0 < d by Z1;
then t1: d - c > 0 by XREAL_1:20;
bb in [.c,d.] by Z1;
then bb in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by s2, RELAT_1:57;
then (TrapezoidalFS (a,b,c,d)) . bb = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . bb by FUNCT_4:13, S1
.= (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . bb by FUNCT_1:49, s0
.= 1 by Cb1, t1 ;
hence TrapezoidalFS (a,b,c,d) is normalized ; :: thesis: verum