set a = z `1 ;
set b = z `2 ;
defpred S₁[ Element of EC_SetAffCo (z,p), set ] means $2 = rep_pt ((compell_ProjCo (z,p)) . $1);
A2: for P being Element of EC_SetAffCo (z,p) ex R being Element of EC_SetAffCo (z,p) st S₁[P,R]

proof

let P be Element of EC_SetAffCo (z,p); :: thesis: ex R being Element of EC_SetAffCo (z,p) st S₁[P,R]
set Q = (compell_ProjCo (z,p)) . P;
reconsider Q = (compell_ProjCo (z,p)) . P as Element of EC_SetProjCo ((z `1),(z `2),p) ;
set R = rep_pt Q;
reconsider R = rep_pt Q as Element of EC_SetAffCo (z,p) by ThAffCo;
take R ; :: thesis: S₁[P,R]
thus S₁[P,R] ; :: thesis: verum

end;

consider f being UnOp of (EC_SetAffCo (z,p)) such that
A3: for P being Element of EC_SetAffCo (z,p) holds S₁[P,f . P] from FUNCT_2:sch 3(A2);
take f ; :: thesis: for P being Element of EC_SetAffCo (z,p) holds f . P = rep_pt ((compell_ProjCo (z,p)) . P)
thus for P being Element of EC_SetAffCo (z,p) holds f . P = rep_pt ((compell_ProjCo (z,p)) . P) by A3; :: thesis: verum