let a, b be real number ; :: 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)
for r, r1, r2 being Real st s = r & r1 = t1 & r2 = t2 holds
(P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (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)
for r, r1, r2 being Real st s = r & r1 = t1 & r2 = t2 holds
(P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))
let t1, t2 be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: for s being Point of (Closed-Interval-TSpace a,b)
for r, r1, r2 being Real st s = r & r1 = t1 & r2 = t2 holds
(P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))
let s be Point of (Closed-Interval-TSpace a,b); :: thesis: for r, r1, r2 being Real st s = r & r1 = t1 & r2 = t2 holds
(P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))
let r, r1, r2 be Real; :: thesis: ( s = r & r1 = t1 & r2 = t2 implies (P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a)) )
assume ( s = r & r1 = t1 & r2 = t2 ) ; :: thesis: (P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))
hence (P[01] a,b,t1,t2) . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) by A1, Def4
.= ((r * (r2 - r1)) + ((b * r1) - (a * r2))) / (b - a)
.= ((r * (r2 - r1)) / (b - a)) + (((b * r1) - (a * r2)) / (b - a)) by XCMPLX_1:63
.= ((r * (r2 - r1)) * (1 / (b - a))) + (((b * r1) - (a * r2)) / (b - a)) by XCMPLX_1:100
.= (((r2 - r1) * (1 / (b - a))) * r) + (((b * r1) - (a * r2)) / (b - a))
.= (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a)) by XCMPLX_1:100 ;
:: thesis: verum