defpred S₁[ 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 S₁[P,Q,R]

proof

let P, Q be Element of EC_SetAffCo (z,p); :: thesis: ex R being Element of EC_SetAffCo (z,p) st S₁[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 ; :: thesis: S₁[P,Q,R]
thus S₁[P,Q,R] ; :: thesis: 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 S₁[P,Q,f . (P,Q)] from BINOP_1:sch 3(A1);
take f ; :: thesis: 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; :: thesis: verum