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