theorem Th26: :: FUZZY_9:20

for p, q, s, t being Real
for f being Function of REAL,REAL st p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 & ( for x being Real holds f . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x ) holds
max+ f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))