let a, b be Real; ( 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
; 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)); ( (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
;
(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
;
verum