theorem Th42: :: EC_PF_2:42

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P)