set a = z `1 ;
set b = z `2 ;
defpred S1[ 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 S1[P,R]
proof
let P be
Element of
EC_SetAffCo (
z,
p);
ex R being Element of EC_SetAffCo (z,p) st S1[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
;
S1[P,R]
thus
S1[
P,
R]
;
verum
end;
consider f being UnOp of (EC_SetAffCo (z,p)) such that
A3:
for P being Element of EC_SetAffCo (z,p) holds S1[P,f . P]
from FUNCT_2:sch 3(A2);
take
f
; 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; verum