set e = L (((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,T st
( f is continuous & f . 0 = a & f . 1 = b ) holds
ex g being Function of I,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,T st
( f is continuous & f . 0 = a & f . 1 = b ) implies ex g being Function of I,T st
( g is continuous & g . 0 = b & g . 1 = a ) )

given P being Function of I,T such that A1: P is continuous and
A2: ( P . 0 = a & P . 1 = b ) ; :: thesis: ex g being Function of I,T st
( g is continuous & g . 0 = b & g . 1 = a )

set f = P * (L (((0,1) (#)),((#) (0,1))));
reconsider f = P * (L (((0,1) (#)),((#) (0,1)))) as Function of I,T by TOPMETR:20;
take f ; :: thesis: ( f is continuous & f . 0 = b & f . 1 = a )
L (((0,1) (#)),((#) (0,1))) is continuous Function of (),() by TREAL_1:8;
hence f is continuous by ; :: thesis: ( f . 0 = b & f . 1 = a )
A3: (L (((0,1) (#)),((#) (0,1)))) . 1 = (L (((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 () by TOPMETR:18;
then A4: 1 in dom (L (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def 1;
0 in [.0,1.] by XXREAL_1:1;
then 0 in the carrier of () by TOPMETR:18;
then A5: 0 in dom (L (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def 1;
(L (((0,1) (#)),((#) (0,1)))) . 0 = (L (((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 ; :: thesis: verum