let a, b be real number ; ( 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 by A2, Lm2;
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:21
.=
((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:128
.=
(((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:77
.=
(((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:77
.=
(((b * r) - (b * a)) + ((b - r) * a)) / (b - a)
by XCMPLX_1:63
.=
((b - a) * r) / (b - a)
.=
c
by A3, XCMPLX_1:90
;
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; 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 by Lm2;
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:21
.=
(((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:90
;
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; verum