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 & 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 e = L[01] (0 ,1 (#) ),((#) 0 ,1);
A2: (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:12
.= 1 by TREAL_1:def 2 ;
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:12
.= 0 by TREAL_1:def 1 ;
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:27;
0 in [.0 ,1.] by XXREAL_1:1;
then 0 in the carrier of (Closed-Interval-TSpace 0 ,1) by TOPMETR:25;
then A4: 0 in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by FUNCT_2:def 1;
1 in [.0 ,1.] by XXREAL_1:1;
then 1 in the carrier of (Closed-Interval-TSpace 0 ,1) by TOPMETR:25;
then A5: 1 in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by FUNCT_2:def 1;
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:11;
hence f is continuous by A1, TOPMETR:27; :: thesis: ( f . 0 = b & f . 1 = a )
thus ( f . 0 = b & f . 1 = a ) by A1, A2, A3, A4, A5, FUNCT_1:23; :: thesis: verum