let p be 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 <> 0 & Q `3_3 <> 0 holds
( rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) iff P _EQ_ (compell_ProjCo (z,p)) . Q )
let z be Element of EC_WParam p; for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 & Q `3_3 <> 0 holds
( rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) iff P _EQ_ (compell_ProjCo (z,p)) . Q )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); ( P `3_3 <> 0 & Q `3_3 <> 0 implies ( rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) iff P _EQ_ (compell_ProjCo (z,p)) . Q ) )
assume A1:
( P `3_3 <> 0 & Q `3_3 <> 0 )
; ( rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) iff P _EQ_ (compell_ProjCo (z,p)) . Q )
set a = z `1 ;
set b = z `2 ;
set CQ = (compell_ProjCo (z,p)) . Q;
reconsider CQ = (compell_ProjCo (z,p)) . Q as Element of EC_SetProjCo ((z `1),(z `2),p) ;
assume
P _EQ_ (compell_ProjCo (z,p)) . Q
; rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q)
hence rep_pt P =
rep_pt CQ
by Th39
.=
(compell_ProjCo (z,p)) . (rep_pt Q)
by A1, Th42
;
verum