let a, b be Real; :: thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds
( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 ) )
assume A1: a <= b ; :: thesis: for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds
( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 )
let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); :: thesis: ( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 )
reconsider r1 = t1, r2 = t2 as Real ;
0 = (#) (0,1) by Def1;
hence (L[01] (t1,t2)) . ((#) (0,1)) = ((1 - 0) * r1) + (0 * r2) by A1, Def3
.= t1 ;
:: thesis: (L[01] (t1,t2)) . ((0,1) (#)) = t2
1 = (0,1) (#) by Def2;
hence (L[01] (t1,t2)) . ((0,1) (#)) = ((1 - 1) * r1) + (1 * r2) by A1, Def3
.= t2 ;
:: thesis: verum