let p be 5 _or_greater Prime; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: ( 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) ;
hereby :: thesis: ( P _EQ_ (compell_ProjCo (z,p)) . Q implies rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) )
assume A2: rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) ; :: thesis: P _EQ_ (compell_ProjCo (z,p)) . Q
rep_pt P = rep_pt CQ by A1, A2, Th42;
hence P _EQ_ (compell_ProjCo (z,p)) . Q by Th39; :: thesis: verum
end;
assume P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis: 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 ;
:: thesis: verum