set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
deffunc H₁( Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]) -> Element of the carrier of (GF p) = ((($1 `2) |^ 2) * ($1 `3)) - (((($1 `1) |^ 3) + ((a * ($1 `1)) * (($1 `3) |^ 2))) + (b * (($1 `3) |^ 3)));
consider f being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):], the carrier of (GF p) such that
P1: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3)))
thus for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) by P1; :: thesis: verum