let a, b be real number ; :: 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 by A1, Lm2;
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