theorem :: FUZZY_8:41

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