let a, b be Real; :: thesis: ( a < b implies 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)) )
assume A1: a < b ; :: thesis: 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))
let t1, t2 be Point of (Closed-Interval-TSpace (0,1)); :: thesis: 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))
let s be Point of (Closed-Interval-TSpace (a,b)); :: thesis: (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
thus (P[01] (a,b,t1,t2)) . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) by A1, Def4
.= ((s * (t2 - t1)) + ((b * t1) - (a * t2))) / (b - a)
.= ((s * (t2 - t1)) / (b - a)) + (((b * t1) - (a * t2)) / (b - a)) by XCMPLX_1:62
.= ((s * (t2 - t1)) * (1 / (b - a))) + (((b * t1) - (a * t2)) / (b - a)) by XCMPLX_1:99
.= (((t2 - t1) * (1 / (b - a))) * s) + (((b * t1) - (a * t2)) / (b - a))
.= (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a)) by XCMPLX_1:99 ; :: thesis: verum