let a, b be Real; ( 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
; ( 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));
((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) * 0) + ((r - a) * 1)) / (b - a)
by A2, A1, 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:15
.=
((1 - ((r - a) / (b - a))) * a) + (((r - a) / (b - a)) * b)
by A2, A4, A5, Def3
.=
((((1 * (b - a)) - (r - a)) / (b - a)) * a) + (((r - a) / (b - a)) * b)
by A3, XCMPLX_1:127
.=
(((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:76
.=
(((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:76
.=
(((a * b) - (a * r)) + ((r - a) * b)) / (b - a)
by XCMPLX_1:62
.=
((b - a) * r) / (b - a)
.=
c
by A3, XCMPLX_1:89
;
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; 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));
((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) * a) + (r * b)
by A2, 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:15
.=
(((b - ((r * (b - a)) + a)) * 0) + ((((r * (b - a)) + a) - a) * 1)) / (b - a)
by A2, A1, A6, Def4
.=
c
by A3, XCMPLX_1:89
;
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; verum