theorem LmCompAddCom: :: EC_PF_3:29

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 = 1 & Q `3_3 = 1 holds
(compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))