set x = the Point of M;
reconsider f = the carrier of M --> the Point of M as Function of the carrier of M, the carrier of M ;
reconsider jd = 1 / 2 as Real ;
take f ; :: thesis: f is contraction
take jd ; :: according to NCFCONT2:def 7 :: thesis: ( 0 < jd & jd < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= jd * ||.(x - y).|| ) )
thus ( 0 < jd & jd < 1 ) ; :: thesis: for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= jd * ||.(x - y).||
let z, y be Point of M; :: thesis: ||.((f . z) - (f . y)).|| <= jd * ||.(z - y).||
( f . z = the Point of M & f . y = the Point of M ) by FUNCOP_1:7;
then A1: ||.((f . z) - (f . y)).|| = 0 by CLVECT_1:107;
||.(z - y).|| >= 0 by CLVECT_1:105;
hence ||.((f . z) - (f . y)).|| <= jd * ||.(z - y).|| by A1; :: thesis: verum