let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
(addell_AffCo (z,p)) . (P,O) = P
let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
(addell_AffCo (z,p)) . (P,O) = P
let P, O be Element of EC_SetAffCo (z,p); :: thesis: ( O = [0,1,0] implies (addell_AffCo (z,p)) . (P,O) = P )
assume A1: O = [0,1,0] ; :: thesis: (addell_AffCo (z,p)) . (P,O) = P
consider PP being Element of EC_SetProjCo ((z `1),(z `2),p) such that
B1: ( PP = P & PP in EC_SetAffCo (z,p) ) ;
(addell_ProjCo (z,p)) . (PP,O) _EQ_ PP by A1, ThUnityProjCo;
then rep_pt ((addell_ProjCo (z,p)) . (PP,O)) = rep_pt PP by EC_PF_2:39
.= PP by B1, ThRepPoint6 ;
hence (addell_AffCo (z,p)) . (P,O) = P by B1, DefAffAddEll; :: thesis: verum