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