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:20;
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:20;
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:20;
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:13
.= P . (((0 - 1) * t) + 1) by A3, TREAL_1:7
.= 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:18;
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:9
.= 1 by TREAL_1:def 2 ;
then A5: f . 0 = P . 1 by A4, FUNCT_1:13
.= 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:18;
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:9
.= 0 by TREAL_1:def 1 ;
then A7: f . 1 = P . 0 by A6, FUNCT_1:13
.= 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:8;
then b,a are_connected by A5, A7, TOPMETR:20;
then reconsider f = f as Path of b,a by A5, A7, A8, Def2, TOPMETR:20;
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