theorem Th11: :: TREAL_1:11

for a, b being Real st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for s being Point of (Closed-Interval-TSpace (a,b)) holds (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))