defpred S1[ Element of EC_SetAffCo (z,p), Element of EC_SetAffCo (z,p), set ] means $3 = rep_pt ((addell_ProjCo (z,p)) . ($1,$2));
A1:
for P, Q being Element of EC_SetAffCo (z,p) ex R being Element of EC_SetAffCo (z,p) st S1[P,Q,R]
proof
let P,
Q be
Element of
EC_SetAffCo (
z,
p);
ex R being Element of EC_SetAffCo (z,p) st S1[P,Q,R]
set R =
rep_pt ((addell_ProjCo (z,p)) . (P,Q));
reconsider R =
rep_pt ((addell_ProjCo (z,p)) . (P,Q)) as
Element of
EC_SetAffCo (
z,
p)
by ThAffCo;
take
R
;
S1[P,Q,R]
thus
S1[
P,
Q,
R]
;
verum
end;
consider f being Function of [:(EC_SetAffCo (z,p)),(EC_SetAffCo (z,p)):],(EC_SetAffCo (z,p)) such that
A2:
for P, Q being Element of EC_SetAffCo (z,p) holds S1[P,Q,f . (P,Q)]
from BINOP_1:sch 3(A1);
take
f
; for P, Q being Element of EC_SetAffCo (z,p) holds f . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q))
thus
for P, Q being Element of EC_SetAffCo (z,p) holds f . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q))
by A2; verum