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

end;

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