let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( P _EQ_ O iff (compell_ProjCo (z,p)) . P _EQ_ O )
let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( P _EQ_ O iff (compell_ProjCo (z,p)) . P _EQ_ O )
let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies ( P _EQ_ O iff (compell_ProjCo (z,p)) . P _EQ_ O ) )
assume A1: O = [0,1,0] ; :: thesis: ( P _EQ_ O iff (compell_ProjCo (z,p)) . P _EQ_ O )

hereby :: thesis: ( (compell_ProjCo (z,p)) . P _EQ_ O implies P _EQ_ O )

assume P _EQ_ O ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ O
then B2: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . O by EC_PF_2:46;
(compell_ProjCo (z,p)) . O _EQ_ O by A1, EC_PF_2:40;
hence (compell_ProjCo (z,p)) . P _EQ_ O by B2, EC_PF_1:44; :: thesis: verum

end;

assume (compell_ProjCo (z,p)) . P _EQ_ O ; :: thesis: P _EQ_ O
then B2: P _EQ_ (compell_ProjCo (z,p)) . O by EC_PF_2:47;
(compell_ProjCo (z,p)) . O _EQ_ O by A1, EC_PF_2:40;
hence P _EQ_ O by B2, EC_PF_1:44; :: thesis: verum