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: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, Th19
;
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