let a, b, c, d, r be Real; :: thesis: ( a < b & b < c & c < d implies TrapezoidalFS (a,b,c,d) = ((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: TrapezoidalFS (a,b,c,d) = ((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((TrapezoidalFS (a,b,c,d)) | [.a,d.])
set f1 = (AffineMap (0,0)) | (REAL \ ].a,d.[);
set f2 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f3 = (AffineMap (0,1)) | [.b,c.];
set f4 = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
thus 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 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.]))) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by FUNCT_4:14
.= ((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 FUNCT_4:14
.= ((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) by LmSymTrape2, A1 ; :: thesis: verum