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 Th18;
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, Th18
;
then A6:
rng (L[01] ((#) a,b),(a,b (#) )) = [#] (Closed-Interval-TSpace a,b)
by FUNCT_2:29;
A7:
rng (L[01] ((#) a,b),(a,b (#) )) = the carrier of (Closed-Interval-TSpace a,b)
by A5, FUNCT_2:29;
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, A7, 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, A7, 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 (#) ) )
A9:
rng (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,1)
by A2, FUNCT_2:29;
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;
A12:
rng (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace 0 ,1)
by A2, FUNCT_2:29;
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 A12, 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 A12, A5, A11, A13, FUNCT_2:36; verum