let a, b be Real; :: 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 )
then A2: b - a <> 0 ;
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 )
reconsider r1 = t1, r2 = t2 as Real ;
a = (#) (a,b) by A1, Def1;
hence (P[01] (a,b,t1,t2)) . ((#) (a,b)) = (((b - a) * r1) + ((a - a) * r2)) / (b - a) by A1, Def4
.= t1 by A2, XCMPLX_1:89 ;
:: 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 A2, XCMPLX_1:89 ;
:: thesis: verum