set a = z `1 ;
set b = z `2 ;
deffunc H1( 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 = H1(x) ) & ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f2 . x = H1(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));
( ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f1 . x = H1(x) ) & ( for x being Element of EC_SetProjCo ((z `1),(z `2),p) holds f2 . x = H1(x) ) implies f1 = f2 )
assume that A3:
for
x being
Element of
EC_SetProjCo (
(z `1),
(z `2),
p) holds
f1 . x = H1(
x)
and A4:
for
x being
Element of
EC_SetProjCo (
(z `1),
(z `2),
p) holds
f2 . x = H1(
x)
;
f1 = f2
hence
f1 = f2
by FUNCT_2:63;
verum
end;
hence
for b1, b2 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 b1 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) & ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b2 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) holds
b1 = b2
; verum