theorem Th15: :: TREAL_1:15

for a, b being Real st a < b holds
( id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) )