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) holds (L[01] t1,t2) . s = ((t2 - t1) * s) + t1 )
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) holds (L[01] t1,t2) . s = ((t2 - t1) * s) + t1
let t1, t2 be Point of (Closed-Interval-TSpace a,b); :: thesis: for s being Point of (Closed-Interval-TSpace 0 ,1) holds (L[01] t1,t2) . s = ((t2 - t1) * s) + t1
let s be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: (L[01] t1,t2) . s = ((t2 - t1) * s) + t1
thus (L[01] t1,t2) . s = ((1 - s) * t1) + (s * t2) by A1, Def3
.= ((t2 - t1) * s) + t1 ; :: thesis: verum