let a, b be real number ; :: thesis: ( 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 (#) ) ) )
assume A1: a < b ; :: thesis: ( 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 (#) );
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 A1, Th18;
then A3: ( L[01] ((#) a,b),(a,b (#) ) is one-to-one & rng (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace 0 ,1) ) by FUNCT_2:29;
A4: rng (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace 0 ,1) by A2, FUNCT_2:29;
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: ( P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) is one-to-one & rng (L[01] ((#) a,b),(a,b (#) )) = the carrier of (Closed-Interval-TSpace a,b) ) by FUNCT_2:29;
A7: rng (L[01] ((#) a,b),(a,b (#) )) = [#] (Closed-Interval-TSpace a,b) by A5, FUNCT_2:29;
A8: dom (L[01] ((#) a,b),(a,b (#) )) = [#] (Closed-Interval-TSpace 0 ,1) by FUNCT_2:def 1;
A9: dom (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) = [#] (Closed-Interval-TSpace a,b) by FUNCT_2:def 1;
A10: (L[01] ((#) a,b),(a,b (#) )) " = (L[01] ((#) a,b),(a,b (#) )) " by A3, A6, TOPS_2:def 4;
A11: (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) " = (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) " by A3, A6, TOPS_2:def 4;
A12: P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) = (L[01] ((#) a,b),(a,b (#) )) " by A2, A3, A6, FUNCT_2:36;
A13: L[01] ((#) a,b),(a,b (#) ) = (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) " by A3, A5, A6, FUNCT_2:36;
A14: L[01] ((#) a,b),(a,b (#) ) is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) by A1, Th11;
A15: L[01] ((#) a,b),(a,b (#) ) is continuous by A1, Th11;
A16: P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) by A1, Th15;
A17: P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) is continuous by A1, Th15;
thus L[01] ((#) a,b),(a,b (#) ) is being_homeomorphism by A3, A7, A8, A10, A12, A15, A16, TOPS_2:def 5; :: thesis: ( (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, A10, FUNCT_2:36; :: thesis: ( 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 P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) is being_homeomorphism by A4, A6, A9, A11, A13, A14, A17, TOPS_2:def 5; :: thesis: (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 A3, A5, A6, A11, FUNCT_2:36; :: thesis: verum