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,((compell_AffCo (z,p)) . P)) = O
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,((compell_AffCo (z,p)) . P)) = O
let P, O be Element of EC_SetAffCo (z,p); :: thesis: ( O = [0,1,0] implies (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O )
assume A1: O = [0,1,0] ; :: thesis: (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O
set Q = (compell_AffCo (z,p)) . P;
reconsider Q = (compell_AffCo (z,p)) . P as Element of EC_SetAffCo (z,p) ;
consider PP being Element of EC_SetProjCo ((z `1),(z `2),p) such that
A2: ( PP = P & PP in EC_SetAffCo (z,p) ) ;
consider OO being Element of EC_SetProjCo ((z `1),(z `2),p) such that
A4: ( OO = O & OO in EC_SetAffCo (z,p) ) ;

per cases ( P `3_3 <> 0 or P `3_3 = 0 ) ;

suppose B1: P `3_3 <> 0 ; :: thesis: (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O

B2: (compell_AffCo (z,p)) . P = rep_pt ((compell_ProjCo (z,p)) . PP) by A2, DefAffCompEll
.= (compell_ProjCo (z,p)) . (rep_pt PP) by A2, B1, EC_PF_2:42
.= (compell_ProjCo (z,p)) . PP by A2, ThRepPoint6 ;
B3: rep_pt ((addell_ProjCo (z,p)) . (PP,((compell_ProjCo (z,p)) . PP))) = (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) by A2, B2, DefAffAddEll;
rep_pt OO = (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) by A1, A4, B3, ThAddCompProjCo, EC_PF_2:39;
hence (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O by A4, ThRepPoint6; :: thesis: verum

end;

suppose P `3_3 = 0 ; :: thesis: (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O

then B2: PP _EQ_ OO by A1, A2, A4, ThEQO;
set COO = (compell_ProjCo (z,p)) . OO;
reconsider COO = (compell_ProjCo (z,p)) . OO as Element of EC_SetProjCo ((z `1),(z `2),p) ;
COO _EQ_ OO by A1, A4, EC_PF_2:40;
then COO _EQ_ PP by B2, EC_PF_1:44;
then (compell_ProjCo (z,p)) . COO _EQ_ (compell_ProjCo (z,p)) . PP by EC_PF_2:46;
then OO _EQ_ (compell_ProjCo (z,p)) . PP by EC_PF_2:41;
then rep_pt ((compell_ProjCo (z,p)) . PP) = rep_pt OO by EC_PF_2:39;
then B4: (compell_AffCo (z,p)) . P = rep_pt OO by A2, DefAffCompEll
.= OO by A4, ThRepPoint6 ;
B5: (addell_ProjCo (z,p)) . (PP,((compell_AffCo (z,p)) . P)) = OO by A1, A4, B2, B4, EC_PF_2:def 9;
thus (addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = rep_pt ((addell_ProjCo (z,p)) . (PP,((compell_AffCo (z,p)) . P))) by A2, DefAffAddEll
.= O by A4, B5, ThRepPoint6 ; :: thesis: verum

end;

end;