let f be Function of X,X; :: thesis: ( f is constant implies f is contraction )
assume A1: f is constant ; :: thesis: f is contraction
set K = 1 / 2;
take 1 / 2 ; :: according to NFCONT_2:def 3 :: thesis: ( not 1 / 2 <= 0 & not 1 <= 1 / 2 & ( for b₁, b₂ being Element of the carrier of X holds ||.((f . b₁) - (f . b₂)).|| <= (1 / 2) * ||.(b₁ - b₂).|| ) )
thus ( 0 < 1 / 2 & 1 / 2 < 1 ) ; :: thesis: for b₁, b₂ being Element of the carrier of X holds ||.((f . b₁) - (f . b₂)).|| <= (1 / 2) * ||.(b₁ - b₂).||
let x, y be Point of X; :: thesis: ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).||
dom f = the carrier of X by FUNCT_2:def 1;
hence ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).|| by NORMSP_1:6, A1, FUNCT_1:def 10; :: thesis: verum