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 Th16;
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, Th16
;
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