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

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