let a, b be real number ; :: 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 (#) )) ) )
assume A1: 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 A2: b - a <> 0 ;
set L = L[01] ((#) a,b),(a,b (#) );
set P = P[01] a,b,((#) 0 ,1),(0 ,1 (#) );
A3: ( 0 = (#) 0 ,1 & 1 = 0 ,1 (#) ) by Def1, Def2;
A4: ( a = (#) a,b & b = a,b (#) ) by A1, 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 by A1, Lm2;
A5: (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) . c = (((b - r) * 0 ) + ((r - a) * 1)) / (b - a) by A1, A3, Def4
.= (r - a) / (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:21
.= ((1 - ((r - a) / (b - a))) * a) + (((r - a) / (b - a)) * b) by A1, A4, A5, Def3
.= ((((1 * (b - a)) - (r - a)) / (b - a)) * a) + (((r - a) / (b - a)) * b) by A2, XCMPLX_1:128
.= (((b - r) / (b - a)) * (a / 1)) + (((r - a) / (b - a)) * b)
.= (((b - r) * a) / (1 * (b - a))) + (((r - a) / (b - a)) * b) by XCMPLX_1:77
.= (((b - r) * a) / (b - a)) + (((r - a) / (b - a)) * (b / 1))
.= (((b - r) * a) / (b - a)) + (((r - a) * b) / (1 * (b - a))) by XCMPLX_1:77
.= (((a * b) - (a * r)) + ((r - a) * b)) / (b - a) by XCMPLX_1:63
.= ((b - a) * r) / (b - a)
.= c by A2, XCMPLX_1:90 ; :: 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 TMAP_1:92; :: 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 by Lm2;
A6: (L[01] ((#) a,b),(a,b (#) )) . c = ((1 - r) * a) + (r * b) by A1, A4, Def3
.= (r * (b - a)) + a ;
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:21
.= (((b - ((r * (b - a)) + a)) * 0 ) + ((((r * (b - a)) + a) - a) * 1)) / (b - a) by A1, A3, A6, Def4
.= c by A2, XCMPLX_1:90 ; :: 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 TMAP_1:92; :: thesis: verum