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