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); :: thesis: (L[01] ((#) 0 ,1),(0 ,1 (#) )) . x = x
reconsider y = x as Real by Lm2;
( (#) 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 ;
:: thesis: verum

end;

hence L[01] ((#) 0 ,1),(0 ,1 (#) ) = id (Closed-Interval-TSpace 0 ,1) by FUNCT_2:201; :: thesis: verum