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;
per cases ( PP `3_3 = 0 or PP `3_3 <> 0 ) ;
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;
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;
end;