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