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 A1: ( 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 A2: L[01] ((#) c,d),(c,d (#) ) is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace c,d) by TREAL_1:11;
P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) by A1, TREAL_1:15;
hence L[01] a,b,c,d is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d) by A2; :: thesis: verum