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_3) |^ 2) * ($1 `3_3)) - (((($1 `1_3) |^ 3) + ((a * ($1 `1_3)) * (($1 `3_3) |^ 2))) + (b * (($1 `3_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
A1: 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_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_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_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A1; :: thesis: verum