set e = L[01] (0 ,1 (#) ),((#) 0 ,1);
reconsider f = P * (L[01] (0 ,1 (#) ),((#) 0 ,1)) as Function of I[01] ,T by TOPMETR:27;
A2: for t being Point of I[01] holds f . t = P . (1 - t)

proof

let t be Point of I[01] ; :: thesis: f . t = P . (1 - t)
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A3: ( 0 ,1 (#) = 1 & (#) 0 ,1 = 0 ) by TREAL_1:def 1, TREAL_1:def 2;
t in the carrier of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
then t in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by FUNCT_2:def 1;
then f . t = P . ((L[01] (0 ,1 (#) ),((#) 0 ,1)) . ee) by FUNCT_1:23
.= P . (((0 - 1) * t) + 1) by A3, TREAL_1:10
.= P . (1 - (1 * t)) ;
hence f . t = P . (1 - t) ; :: thesis: verum

end;

0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 0 in [.0 ,1.] by RCOMP_1:def 1;
then 0 in the carrier of (Closed-Interval-TSpace 0 ,1) by TOPMETR:25;
then A4: 0 in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by FUNCT_2:def 1;
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . 0 = (L[01] (0 ,1 (#) ),((#) 0 ,1)) . ((#) 0 ,1) by TREAL_1:def 1
.= 0 ,1 (#) by TREAL_1:12
.= 1 by TREAL_1:def 2 ;
then A5: f . 0 = P . 1 by A4, FUNCT_1:23
.= b by A1, Def2 ;
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 1 in [.0 ,1.] by RCOMP_1:def 1;
then 1 in the carrier of (Closed-Interval-TSpace 0 ,1) by TOPMETR:25;
then A6: 1 in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by FUNCT_2:def 1;
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . 1 = (L[01] (0 ,1 (#) ),((#) 0 ,1)) . (0 ,1 (#) ) by TREAL_1:def 2
.= (#) 0 ,1 by TREAL_1:12
.= 0 by TREAL_1:def 1 ;
then A7: f . 1 = P . 0 by A6, FUNCT_1:23
.= a by A1, Def2 ;
A8: ( P is continuous & L[01] (0 ,1 (#) ),((#) 0 ,1) is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace 0 ,1) ) by A1, Def2, TREAL_1:11;
then b,a are_connected by A5, A7, Def1, TOPMETR:27;
then reconsider f = f as Path of b,a by A5, A7, A8, Def2, TOPMETR:27;
take f ; :: thesis: for t being Point of I[01] holds f . t = P . (1 - t)
thus for t being Point of I[01] holds f . t = P . (1 - t) by A2; :: thesis: verum