for x being Point of (Closed-Interval-TSpace (0,1)) holds (P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x = x
proof
let x be
Point of
(Closed-Interval-TSpace (0,1));
(P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x = x
reconsider y =
x as
Real ;
(
(#) (
0,1)
= 0 & (
0,1)
(#) = 1 )
by Def1, Def2;
hence (P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x =
(((1 - y) * 0) + ((y - 0) * 1)) / (1 - 0)
by Def4
.=
x
;
verum
end;
hence
P[01] (0,1,((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1))
by FUNCT_2:124; verum