theorem Th23a: :: FUZZY_8:36

for a, b, c, d, r, s being Real st a < b & b < c & c < d holds
( (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . a = 0 & (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . d = 0 )