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 NFCONT_2:def 3 :: 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 NORMSP_1:6;

thus ||.((f . z) - (f . y)).|| <= jd * ||.(z - y).|| by A1; :: thesis: verum

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 NFCONT_2:def 3 :: 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 NORMSP_1:6;

thus ||.((f . z) - (f . y)).|| <= jd * ||.(z - y).|| by A1; :: thesis: verum