set a = z `1 ;
set b = z `2 ;
defpred S₁[ Element of EC_SetProjCo ((z `1),(z `2),p), set ] means $2 = [($1 `1_3),(- ($1 `2_3)),($1 `3_3)];
A1: for P being Element of EC_SetProjCo ((z `1),(z `2),p) ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S₁[P,R]

proof

let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S₁[P,R]
set R = [(P `1_3),(- (P `2_3)),(P `3_3)];
[(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p) by Lm1;
hence ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S₁[P,R] ; :: thesis: verum

end;

consider f being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) such that
A2: for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds S₁[P,f . P] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds f . P = [(P `1_3),(- (P `2_3)),(P `3_3)]
thus for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds f . P = [(P `1_3),(- (P `2_3)),(P `3_3)] by A2; :: thesis: verum