set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
deffunc H1( 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 = H1(x)
from FUNCT_2:sch 4();
take
f
; 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; verum