set a = z `1 ;

set b = z `2 ;

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

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

set b = z `2 ;

defpred S

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

proof

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

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

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

thus S

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

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