let a, b be real number ; ( a < b implies ( L[01] (a,b (#) ),((#) a,b) is being_homeomorphism & (L[01] (a,b (#) ),((#) a,b)) " = P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) & P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism & (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),((#) a,b) ) )
set L = L[01] (a,b (#) ),((#) a,b);
set P = P[01] a,b,(0 ,1 (#) ),((#) 0 ,1);
assume A1:
a < b
; ( L[01] (a,b (#) ),((#) a,b) is being_homeomorphism & (L[01] (a,b (#) ),((#) a,b)) " = P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) & P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism & (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),((#) a,b) )
then A2:
id the carrier of (Closed-Interval-TSpace 0 ,1) = (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) * (L[01] (a,b (#) ),((#) a,b))
by Th19;
then A3:
L[01] (a,b (#) ),((#) a,b) is one-to-one
by FUNCT_2:29;
A4:
( L[01] (a,b (#) ),((#) a,b) is continuous & P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) )
by A1, Th11, Th15;
A5: id the carrier of (Closed-Interval-TSpace a,b) =
id (Closed-Interval-TSpace a,b)
.=
(L[01] (a,b (#) ),((#) a,b)) * (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1))
by A1, Th19
;
then
L[01] (a,b (#) ),((#) a,b) is onto
by FUNCT_2:29;
then A6:
rng (L[01] (a,b (#) ),((#) a,b)) = [#] (Closed-Interval-TSpace a,b)
by FUNCT_2:def 3;
then
rng (L[01] (a,b (#) ),((#) a,b)) = the carrier of (Closed-Interval-TSpace a,b)
;
then A8:
(L[01] (a,b (#) ),((#) a,b)) " = (L[01] (a,b (#) ),((#) a,b)) "
by A3, TOPS_2:def 4;
( dom (L[01] (a,b (#) ),((#) a,b)) = [#] (Closed-Interval-TSpace 0 ,1) & P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) = (L[01] (a,b (#) ),((#) a,b)) " )
by A2, A3, A6, FUNCT_2:36, FUNCT_2:def 1;
hence
L[01] (a,b (#) ),((#) a,b) is being_homeomorphism
by A3, A6, A8, A4, TOPS_2:def 5; ( (L[01] (a,b (#) ),((#) a,b)) " = P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) & P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism & (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),((#) a,b) )
thus
(L[01] (a,b (#) ),((#) a,b)) " = P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)
by A2, A3, A6, A8, FUNCT_2:36; ( P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism & (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),((#) a,b) )
P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is onto
by A2, FUNCT_2:29;
then A9:
rng (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) = [#] (Closed-Interval-TSpace 0 ,1)
by FUNCT_2:def 3;
A10:
( L[01] (a,b (#) ),((#) a,b) is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) & P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is continuous )
by A1, Th11, Th15;
A11:
P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is one-to-one
by A5, FUNCT_2:29;
rng (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) = the carrier of (Closed-Interval-TSpace 0 ,1)
by A9;
then A13:
(P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) "
by A11, TOPS_2:def 4;
( dom (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) = [#] (Closed-Interval-TSpace a,b) & L[01] (a,b (#) ),((#) a,b) = (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " )
by A9, A5, A11, FUNCT_2:36, FUNCT_2:def 1;
hence
P[01] a,b,(0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism
by A9, A11, A13, A10, TOPS_2:def 5; (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),((#) a,b)
thus
(P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),((#) a,b)
by A9, A5, A11, A13, FUNCT_2:36; verum