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) * 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
;
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) * 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
;
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