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
( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )
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
( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )
let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies ( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P ) )
assume A1: O = [0,1,0] ; :: thesis: ( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )
(addell_ProjCo (z,p)) . (P,O) _EQ_ P

proof

per cases ( P _EQ_ O or not P _EQ_ O ) ;

suppose B1: P _EQ_ O ; :: thesis: (addell_ProjCo (z,p)) . (P,O) _EQ_ P

then (addell_ProjCo (z,p)) . (P,O) = O by A1, EC_PF_2:def 9;
hence (addell_ProjCo (z,p)) . (P,O) _EQ_ P by B1; :: thesis: verum

end;

suppose not P _EQ_ O ; :: thesis: (addell_ProjCo (z,p)) . (P,O) _EQ_ P

hence (addell_ProjCo (z,p)) . (P,O) _EQ_ P by A1, EC_PF_2:def 9; :: thesis: verum

end;

end;

end;

hence ( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P ) by A1, EC_PF_2:def 9; :: thesis: verum