let a, b, c, d be real number ; :: 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:11, TREAL_1:15;
hence L[01] a,b,c,d is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d) ; :: thesis: verum