let a, b, c, d be real number ; :: thesis: ( a < b & c < d implies ( (L[01] a,b,c,d) . a = c & (L[01] a,b,c,d) . b = d ) )
assume that
A1: a < b and
A2: c < d ; :: thesis: ( (L[01] a,b,c,d) . a = c & (L[01] a,b,c,d) . b = d )
a in [.a,b.] by A1, XXREAL_1:1;
then a in the carrier of (Closed-Interval-TSpace a,b) by A1, TOPMETR:25;
then a in dom (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) by FUNCT_2:def 1;
hence (L[01] a,b,c,d) . a = (L[01] ((#) c,d),(c,d (#) )) . ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) . a) by FUNCT_1:23
.= (L[01] ((#) c,d),(c,d (#) )) . ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) . ((#) a,b)) by A1, TREAL_1:def 1
.= (L[01] ((#) c,d),(c,d (#) )) . ((#) 0 ,1) by A1, TREAL_1:16
.= (#) c,d by A2, TREAL_1:12
.= c by A2, TREAL_1:def 1 ;
:: thesis: (L[01] a,b,c,d) . b = d
b in [.a,b.] by A1, XXREAL_1:1;
then b in the carrier of (Closed-Interval-TSpace a,b) by A1, TOPMETR:25;
then b in dom (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) by FUNCT_2:def 1;
hence (L[01] a,b,c,d) . b = (L[01] ((#) c,d),(c,d (#) )) . ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) . b) by FUNCT_1:23
.= (L[01] ((#) c,d),(c,d (#) )) . ((P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) . (a,b (#) )) by A1, TREAL_1:def 2
.= (L[01] ((#) c,d),(c,d (#) )) . (0 ,1 (#) ) by A1, TREAL_1:16
.= c,d (#) by A2, TREAL_1:12
.= d by A2, TREAL_1:def 2 ;
:: thesis: verum