deffunc H₁( Point of X) -> Element of the carrier of X = r * $1;
consider F being Function of the carrier of X, the carrier of X such that
A1: for x being Point of X holds F . x = H₁(x) from FUNCT_2:sch 4();
reconsider F = F as Function of X,X ;
take F ; :: thesis: for x being Point of X holds F . x = r * x
thus for x being Point of X holds F . x = r * x by A1; :: thesis: verum