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)));
let f, g be Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):], the carrier of (GF p); :: 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))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds g . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) ) implies f = g )
assume 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) ; :: thesis: ( ex P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st not g . P = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) or f = g )
assume P2: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds g . x = H₁(x) ; :: thesis: f = g

now

let x be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; :: thesis: f . x = g . x
thus f . x = H₁(x) by P1
.= g . x by P2 ; :: thesis: verum

end;

hence f = g by FUNCT_2:def 8; :: thesis: verum