defpred S_{1}[ 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_{1}[P,Q,R]

A2: for P, Q being Element of EC_SetAffCo (z,p) holds S_{1}[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

A1: for P, Q being Element of EC_SetAffCo (z,p) ex R being Element of EC_SetAffCo (z,p) st S

proof

consider f being Function of [:(EC_SetAffCo (z,p)),(EC_SetAffCo (z,p)):],(EC_SetAffCo (z,p)) such that
let P, Q be Element of EC_SetAffCo (z,p); :: thesis: ex R being Element of EC_SetAffCo (z,p) st S_{1}[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_{1}[P,Q,R]

thus S_{1}[P,Q,R]
; :: thesis: verum

end;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

thus S

A2: for P, Q being Element of EC_SetAffCo (z,p) holds S

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