let a, b be Real; :: thesis: ( a < b implies ( id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) ) )
A1: ( 0 = (#) (0,1) & 1 = (0,1) (#) ) by Def1, Def2;
set L = L[01] (((a,b) (#)),((#) (a,b)));
set P = P[01] (a,b,((0,1) (#)),((#) (0,1)));
assume A2: a < b ; :: thesis: ( id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) )
then A3: b - a <> 0 ;
A4: ( a = (#) (a,b) & b = (a,b) (#) ) by A2, Def1, Def2;
for c being Point of (Closed-Interval-TSpace (a,b)) holds ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = c

proof

let c be Point of (Closed-Interval-TSpace (a,b)); :: thesis: ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = c
reconsider r = c as Real ;
A5: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) . c = (((b - r) * 1) + ((r - a) * 0)) / (b - a) by A2, A1, Def4
.= (b - r) / (b - a) ;
thus ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = (L[01] (((a,b) (#)),((#) (a,b)))) . ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) . c) by FUNCT_2:15
.= ((1 - ((b - r) / (b - a))) * b) + (((b - r) / (b - a)) * a) by A2, A4, A5, Def3
.= ((((1 * (b - a)) - (b - r)) / (b - a)) * b) + (((b - r) / (b - a)) * a) by A3, XCMPLX_1:127
.= (((r - a) / (b - a)) * (b / 1)) + (((b - r) / (b - a)) * a)
.= (((r - a) * b) / (1 * (b - a))) + (((b - r) / (b - a)) * a) by XCMPLX_1:76
.= (((r - a) * b) / (b - a)) + (((b - r) / (b - a)) * (a / 1))
.= (((r - a) * b) / (b - a)) + (((b - r) * a) / (1 * (b - a))) by XCMPLX_1:76
.= (((b * r) - (b * a)) + ((b - r) * a)) / (b - a) by XCMPLX_1:62
.= ((b - a) * r) / (b - a)
.= c by A3, XCMPLX_1:89 ; :: thesis: verum

end;

hence id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) by FUNCT_2:124; :: thesis: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))
for c being Point of (Closed-Interval-TSpace (0,1)) holds ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = c

proof

let c be Point of (Closed-Interval-TSpace (0,1)); :: thesis: ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = c
reconsider r = c as Real ;
A6: (L[01] (((a,b) (#)),((#) (a,b)))) . c = ((1 - r) * b) + (r * a) by A2, A4, Def3
.= (r * (a - b)) + b ;
thus ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) . ((L[01] (((a,b) (#)),((#) (a,b)))) . c) by FUNCT_2:15
.= (((b - ((r * (a - b)) + b)) * 1) + ((((r * (a - b)) + b) - a) * 0)) / (b - a) by A2, A1, A6, Def4
.= (r * (- (a - b))) / (b - a)
.= c by A3, XCMPLX_1:89 ; :: thesis: verum

end;

hence id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) by FUNCT_2:124; :: thesis: verum