let a, b be real number ; :: thesis: ( a < b implies for t1, t2 being Point of (Closed-Interval-TSpace 0 ,1) holds
( (P[01] a,b,t1,t2) . ((#) a,b) = t1 & (P[01] a,b,t1,t2) . (a,b (#) ) = t2 ) )
assume A1: a < b ; :: thesis: for t1, t2 being Point of (Closed-Interval-TSpace 0 ,1) holds
( (P[01] a,b,t1,t2) . ((#) a,b) = t1 & (P[01] a,b,t1,t2) . (a,b (#) ) = t2 )
let t1, t2 be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: ( (P[01] a,b,t1,t2) . ((#) a,b) = t1 & (P[01] a,b,t1,t2) . (a,b (#) ) = t2 )
A2: a = (#) a,b by A1, Def1;
reconsider r1 = t1, r2 = t2 as Real by Lm2;
A3: b - a <> 0 by A1;
thus (P[01] a,b,t1,t2) . ((#) a,b) = (((b - a) * r1) + ((a - a) * r2)) / (b - a) by A1, A2, Def4
.= t1 by A3, XCMPLX_1:90 ; :: thesis: (P[01] a,b,t1,t2) . (a,b (#) ) = t2
b = a,b (#) by A1, Def2;
hence (P[01] a,b,t1,t2) . (a,b (#) ) = (((b - b) * r1) + ((b - a) * r2)) / (b - a) by A1, Def4
.= t2 by A3, XCMPLX_1:90 ;
:: thesis: verum