set e = L[01] (((0,1) (#)),((#) (0,1)));

let T be non empty TopSpace; :: thesis: for a, b being Point of T st ex f being Function of I[01],T st

( f is continuous & f . 0 = a & f . 1 = b ) holds

ex g being Function of I[01],T st

( g is continuous & g . 0 = b & g . 1 = a )

let a, b be Point of T; :: thesis: ( ex f being Function of I[01],T st

( f is continuous & f . 0 = a & f . 1 = b ) implies ex g being Function of I[01],T st

( g is continuous & g . 0 = b & g . 1 = a ) )

given P being Function of I[01],T such that A1: P is continuous and

A2: ( P . 0 = a & P . 1 = b ) ; :: thesis: ex g being Function of I[01],T st

( g is continuous & g . 0 = b & g . 1 = a )

set f = P * (L[01] (((0,1) (#)),((#) (0,1))));

reconsider f = P * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],T by TOPMETR:20;

take f ; :: thesis: ( f is continuous & f . 0 = b & f . 1 = a )

L[01] (((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (0,1)) by TREAL_1:8;

hence f is continuous by A1, TOPMETR:20; :: thesis: ( f . 0 = b & f . 1 = a )

A3: (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 ;

1 in [.0,1.] by XXREAL_1:1;

then 1 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;

then A4: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def 1;

0 in [.0,1.] by XXREAL_1:1;

then 0 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;

then A5: 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 ;

hence ( f . 0 = b & f . 1 = a ) by A2, A3, A5, A4, FUNCT_1:13; :: thesis: verum

let T be non empty TopSpace; :: thesis: for a, b being Point of T st ex f being Function of I[01],T st

( f is continuous & f . 0 = a & f . 1 = b ) holds

ex g being Function of I[01],T st

( g is continuous & g . 0 = b & g . 1 = a )

let a, b be Point of T; :: thesis: ( ex f being Function of I[01],T st

( f is continuous & f . 0 = a & f . 1 = b ) implies ex g being Function of I[01],T st

( g is continuous & g . 0 = b & g . 1 = a ) )

given P being Function of I[01],T such that A1: P is continuous and

A2: ( P . 0 = a & P . 1 = b ) ; :: thesis: ex g being Function of I[01],T st

( g is continuous & g . 0 = b & g . 1 = a )

set f = P * (L[01] (((0,1) (#)),((#) (0,1))));

reconsider f = P * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],T by TOPMETR:20;

take f ; :: thesis: ( f is continuous & f . 0 = b & f . 1 = a )

L[01] (((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (0,1)) by TREAL_1:8;

hence f is continuous by A1, TOPMETR:20; :: thesis: ( f . 0 = b & f . 1 = a )

A3: (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 ;

1 in [.0,1.] by XXREAL_1:1;

then 1 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;

then A4: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def 1;

0 in [.0,1.] by XXREAL_1:1;

then 0 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;

then A5: 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 ;

hence ( f . 0 = b & f . 1 = a ) by A2, A3, A5, A4, FUNCT_1:13; :: thesis: verum