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) st P `3_3 = 0 holds
P _EQ_ (compell_ProjCo (z,p)) . P
let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 = 0 holds
P _EQ_ (compell_ProjCo (z,p)) . P
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P `3_3 = 0 implies P _EQ_ (compell_ProjCo (z,p)) . P )
set a = z `1 ;
set b = z `2 ;
set O = [0,1,0];
reconsider O = [0,1,0] as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
assume A2: P `3_3 = 0 ; :: thesis: P _EQ_ (compell_ProjCo (z,p)) . P
A3: (compell_ProjCo (z,p)) . O _EQ_ O by EC_PF_2:40;
A4: P _EQ_ O by A2, ThEQO;
then (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . O by EC_PF_2:46;
then (compell_ProjCo (z,p)) . P _EQ_ O by A3, EC_PF_1:44;
hence P _EQ_ (compell_ProjCo (z,p)) . P by A4, EC_PF_1:44; :: thesis: verum