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)

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

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

0 in { r where r is Real : ( 0 <= r & r <= 1 ) }
;
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;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

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