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)));
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_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_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_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) implies f = g )
assume A2: 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_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) or f = g )
assume A3: 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 :: thesis: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . x = g . x

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 A2
.= g . x by A3 ; :: thesis: verum

end;

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