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:23;
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 B1:
L[01] (((#) (a,b)),((a,b) (#))) is onto
by FUNCT_2:23;
then A6:
rng (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (a,b))
by FUNCT_2:def 3;
A7:
(L[01] (((#) (a,b)),((a,b) (#)))) " = (L[01] (((#) (a,b)),((a,b) (#)))) "
by A3, B1, 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:30, FUNCT_2:def 1;
hence
L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism
by A3, A6, A7, 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, A7, FUNCT_2:30; ( 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) (#))) )
B1:
P[01] (a,b,((#) (0,1)),((0,1) (#))) is onto
by A2, FUNCT_2:23;
then A8:
rng (P[01] (a,b,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,1))
by FUNCT_2:def 3;
A9:
( 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;
A10:
P[01] (a,b,((#) (0,1)),((0,1) (#))) is one-to-one
by A5, FUNCT_2:23;
A11:
(P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) "
by A10, B1, 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 A8, A5, A10, FUNCT_2:30, FUNCT_2:def 1;
hence
P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism
by A8, A10, A11, A9, 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 A8, A5, A10, A11, FUNCT_2:30; verum