let a, b be Real; :: 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