let r1, r2, r3, r4, r5, r6 be Real; :: thesis: ( r1 < r2 & r3 <= r4 & r5 < r6 implies (L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4) )
set f1 = L[01] (r1,r2,r3,r4);
set f2 = L[01] (r5,r6,r1,r2);
set f3 = L[01] (r5,r6,r3,r4);
assume A1: ( r1 < r2 & r3 <= r4 & r5 < r6 ) ; :: thesis: (L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4)
A2: dom ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) = [#] (Closed-Interval-TSpace (r5,r6)) by FUNCT_2:def 1
.= dom (L[01] (r5,r6,r3,r4)) by FUNCT_2:def 1 ;
for x being object st x in dom ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) holds
((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) . x = (L[01] (r5,r6,r3,r4)) . x

proof

let x be object ; :: thesis: ( x in dom ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) implies ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) . x = (L[01] (r5,r6,r3,r4)) . x )
assume A3: x in dom ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) ; :: thesis: ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) . x = (L[01] (r5,r6,r3,r4)) . x
then A4: x in [#] (Closed-Interval-TSpace (r5,r6)) ;
then A5: x in [.r5,r6.] by A1, TOPMETR:18;
reconsider r = x as Real by A3;
A6: ( r5 <= r & r <= r6 ) by A5, XXREAL_1:1;
A7: rng (L[01] (r5,r6,r1,r2)) c= [#] (Closed-Interval-TSpace (r1,r2)) by RELAT_1:def 19;
reconsider s = (L[01] (r5,r6,r1,r2)) . x as Real ;
x in dom (L[01] (r5,r6,r1,r2)) by A4, FUNCT_2:def 1;
then s in [#] (Closed-Interval-TSpace (r1,r2)) by A7, FUNCT_1:3;
then s in [.r1,r2.] by A1, TOPMETR:18;
then ( r1 <= s & s <= r2 ) by XXREAL_1:1;
then A8: (L[01] (r1,r2,r3,r4)) . s = (((r4 - r3) / (r2 - r1)) * (s - r1)) + r3 by A1, BORSUK_6:35;
A9: r2 - r1 <> 0 by A1;
A10: ((r4 - r3) / (r2 - r1)) * s = ((r4 - r3) / (r2 - r1)) * ((((r2 - r1) / (r6 - r5)) * (r - r5)) + r1) by A1, A6, BORSUK_6:35
.= ((((r4 - r3) / (r2 - r1)) * ((r2 - r1) / (r6 - r5))) * (r - r5)) + (((r4 - r3) / (r2 - r1)) * r1)
.= ((((r4 - r3) / (r6 - r5)) * ((r2 - r1) / (r2 - r1))) * (r - r5)) + (((r4 - r3) / (r2 - r1)) * r1) by XCMPLX_1:85
.= ((((r4 - r3) / (r6 - r5)) * 1) * (r - r5)) + (((r4 - r3) / (r2 - r1)) * r1) by A9, XCMPLX_1:60
.= (((r4 - r3) / (r6 - r5)) * (r - r5)) + (((r4 - r3) / (r2 - r1)) * r1) ;
thus ((L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2))) . x = (L[01] (r1,r2,r3,r4)) . ((L[01] (r5,r6,r1,r2)) . x) by A3, FUNCT_1:12
.= (L[01] (r5,r6,r3,r4)) . x by A10, A8, A1, A6, BORSUK_6:35 ; :: thesis: verum

end;

hence (L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4) by A2, FUNCT_1:2; :: thesis: verum