theorem SymTrape: :: FUZZY_7:47

for a1, c, a2, d being Real st c > 0 & d > 0 & a1 < a2 holds
(((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)']