:: deftheorem Def4 defines P[01] TREAL_1:def 4 :
for a, b being Real st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for b₅ being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) holds
( b₅ = P[01] (a,b,t1,t2) iff for s being Point of (Closed-Interval-TSpace (a,b)) holds b₅ . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );