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 _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),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 _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )
set a = z `1 ;
set b = z `2 ;
A1: ( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) ) by Th30;
consider PP being Element of ProjCo (GF p) such that
A2: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;

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

suppose P `3_3 = 0 ; :: thesis: ( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )

then A3: PP `3_3 = 0 by A2, Th32;
consider Q being Element of ProjCo (GF p) such that
A4: ( Q in EC_SetProjCo ((z `1),(z `2),p) & Q _EQ_ PP ) and
A5: ( Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) by A1, A2, A3, EC_PF_1:49;
rep_pt PP = [0,1,0] by A3, Def7;
hence ( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) ) by A2, A4, A5, AA; :: thesis: verum

end;

suppose P `3_3 <> 0 ; :: thesis: ( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )

then A6: PP `3_3 <> 0 by A2, Th32;
consider Q being Element of ProjCo (GF p) such that
A7: ( Q in EC_SetProjCo ((z `1),(z `2),p) & Q _EQ_ PP ) and
A8: Q `3_3 = 1 by A1, A2, A6, EC_PF_1:48;
consider d being Element of (GF p) such that
d <> 0. (GF p) and
A9: ( Q `1_3 = d * (PP `1_3) & Q `2_3 = d * (PP `2_3) & Q `3_3 = d * (PP `3_3) ) by A7, EC_PF_1:def 10;
A10: d * (PP `3_3) = 1. (GF p) by A8, A9, EC_PF_1:12;
PP `3_3 <> 0. (GF p) by A6, EC_PF_1:11;
then d = (PP `3_3) " by A10, VECTSP_1:def 10;
then Q = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by A8, A9, AA;
hence ( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) ) by A2, A6, A7, Def7; :: thesis: verum

end;

end;