theorem LmSymTrape4: :: FUZZY_7:46

for a, b, c, d, r being Real st a < b & b < c & c < d holds
(((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) = (r (#) (TrapezoidalFS (a,b,c,d))) | [.a,d.]