set a = z `1 ;
set b = z `2 ;
deffunc H₁( Element of EC_SetProjCo ((z `1),(z `2),p)) -> Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] = [($1 `1_3),(- ($1 `2_3)),($1 `3_3)];
for f1, f2 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) st ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f1 . x = H<sub>1</sub>(x) ) & ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f2 . x = H₁(x) ) holds
f1 = f2

proof

let f1, f2 be Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)); :: thesis: ( ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f1 . x = H₁(x) ) & ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f2 . x = H₁(x) ) implies f1 = f2 )
assume that
A1: for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f1 . x = H₁(x) and
A2: for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f2 . x = H₁(x) ; :: thesis: f1 = f2

now :: thesis: for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f1 . x = f2 . x

let x be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: f1 . x = f2 . x
thus f1 . x = H₁(x) by A1
.= f2 . x by A2 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum

end;

hence for b₁, b₂ being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) st ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b₁ . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) & ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b<sub>2</sub> . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) holds
b₁ = b₂ ; :: thesis: verum