let a, b, c, d be Real; :: thesis: ( a < b & c <= d implies L[01] (a,b,c,d) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) )
assume ( a < b & c <= d ) ; :: thesis: L[01] (a,b,c,d) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
then ( L[01] (((#) (c,d)),((c,d) (#))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (c,d)) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) ) by TREAL_1:8, TREAL_1:12;
hence L[01] (a,b,c,d) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) ; :: thesis: verum