set a = z `1 ;
set b = z `2 ;
deffunc H1( Element of EC_SetAffCo (z,p)) -> Element of ProjCo (GF p) = rep_pt ((compell_ProjCo (z,p)) . \$1);
for f1, f2 being UnOp of (EC_SetAffCo (z,p)) st ( for x being Element of EC_SetAffCo (z,p) holds f1 . x = H1(x) ) & ( for x being Element of EC_SetAffCo (z,p) holds f2 . x = H1(x) ) holds
f1 = f2
proof
let f1, f2 be UnOp of (EC_SetAffCo (z,p)); :: thesis: ( ( for x being Element of EC_SetAffCo (z,p) holds f1 . x = H1(x) ) & ( for x being Element of EC_SetAffCo (z,p) holds f2 . x = H1(x) ) implies f1 = f2 )
assume that
A2: for x being Element of EC_SetAffCo (z,p) holds f1 . x = H1(x) and
A3: for x being Element of EC_SetAffCo (z,p) holds f2 . x = H1(x) ; :: thesis: f1 = f2
now :: thesis: for x being Element of EC_SetAffCo (z,p) holds f1 . x = f2 . x
let x be Element of EC_SetAffCo (z,p); :: thesis: f1 . x = f2 . x
thus f1 . x = H1(x) by A2
.= f2 . x by A3 ; :: thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; :: thesis: verum
end;
hence for b1, b2 being UnOp of (EC_SetAffCo (z,p)) st ( for P being Element of EC_SetAffCo (z,p) holds b1 . P = rep_pt ((compell_ProjCo (z,p)) . P) ) & ( for P being Element of EC_SetAffCo (z,p) holds b2 . P = rep_pt ((compell_ProjCo (z,p)) . P) ) holds
b1 = b2 ; :: thesis: verum