let a, b be real number ; :: thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace a,b)
for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
(L[01] t1,t2) . s = ((r2 - r1) * r) + r1 )
assume A1: a <= b ; :: thesis: for t1, t2 being Point of (Closed-Interval-TSpace a,b)
for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
(L[01] t1,t2) . s = ((r2 - r1) * r) + r1
let t1, t2 be Point of (Closed-Interval-TSpace a,b); :: thesis: for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
(L[01] t1,t2) . s = ((r2 - r1) * r) + r1
let s be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
(L[01] t1,t2) . s = ((r2 - r1) * r) + r1
let r, r1, r2 be real number ; :: thesis: ( s = r & r1 = t1 & r2 = t2 implies (L[01] t1,t2) . s = ((r2 - r1) * r) + r1 )
assume ( s = r & r1 = t1 & r2 = t2 ) ; :: thesis: (L[01] t1,t2) . s = ((r2 - r1) * r) + r1
hence (L[01] t1,t2) . s = ((1 - r) * r1) + (r * r2) by A1, Def3
.= ((r2 - r1) * r) + r1 ;
:: thesis: verum