let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p

for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds rep_pt P is Element of EC_SetAffCo (z,p)

let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds rep_pt P is Element of EC_SetAffCo (z,p)

let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: rep_pt P is Element of EC_SetAffCo (z,p)

set a = z `1 ;

set b = z `2 ;

consider PP being Element of ProjCo (GF p) such that

A2: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;

consider Q being Element of ProjCo (GF p) such that

A3: Q = rep_pt P ;

reconsider Q = Q as Element of EC_SetProjCo ((z `1),(z `2),p) by A3, EC_PF_2:36;

for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds rep_pt P is Element of EC_SetAffCo (z,p)

let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds rep_pt P is Element of EC_SetAffCo (z,p)

let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: rep_pt P is Element of EC_SetAffCo (z,p)

set a = z `1 ;

set b = z `2 ;

consider PP being Element of ProjCo (GF p) such that

A2: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;

consider Q being Element of ProjCo (GF p) such that

A3: Q = rep_pt P ;

reconsider Q = Q as Element of EC_SetProjCo ((z `1),(z `2),p) by A3, EC_PF_2:36;

per cases
( PP `3_3 = 0 or PP `3_3 <> 0 )
;

end;

suppose
PP `3_3 = 0
; :: thesis: rep_pt P is Element of EC_SetAffCo (z,p)

then B1:
Q = [0,1,0]
by A2, A3, EC_PF_2:def 7;

Q in { QQ where QQ is Element of EC_SetProjCo ((z `1),(z `2),p) : ( QQ `3_3 = 1 or QQ = [0,1,0] ) } by B1;

hence rep_pt P is Element of EC_SetAffCo (z,p) by A3; :: thesis: verum

end;Q in { QQ where QQ is Element of EC_SetProjCo ((z `1),(z `2),p) : ( QQ `3_3 = 1 or QQ = [0,1,0] ) } by B1;

hence rep_pt P is Element of EC_SetAffCo (z,p) by A3; :: thesis: verum

suppose
PP `3_3 <> 0
; :: thesis: rep_pt P is Element of EC_SetAffCo (z,p)

then
rep_pt PP = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1]
by EC_PF_2:def 7;

then B1: Q `3_3 = 1 by A2, A3, EC_PF_2:def 5;

Q in { QQ where QQ is Element of EC_SetProjCo ((z `1),(z `2),p) : ( QQ `3_3 = 1 or QQ = [0,1,0] ) } by B1;

hence rep_pt P is Element of EC_SetAffCo (z,p) by A3; :: thesis: verum

end;then B1: Q `3_3 = 1 by A2, A3, EC_PF_2:def 5;

Q in { QQ where QQ is Element of EC_SetProjCo ((z `1),(z `2),p) : ( QQ `3_3 = 1 or QQ = [0,1,0] ) } by B1;

hence rep_pt P is Element of EC_SetAffCo (z,p) by A3; :: thesis: verum