let a, b, c, d be Real; :: 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:18;
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:13
.= (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:13
.= (#) (c,d) by A2, TREAL_1:9
.= 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:18;
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:13
.= (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:13
.= (c,d) (#) by A2, TREAL_1:9
.= d by A2, TREAL_1:def 2 ;
:: thesis: verum