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) holds
( P = Q iff (compell_ProjCo (z,p)) . P = (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) holds
( P = Q iff (compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); ( P = Q iff (compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q )
thus
( P = Q implies (compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q )
; ( (compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q implies P = Q )
assume A1:
(compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q
; P = Q
thus P =
(compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . Q)
by A1, Th41
.=
Q
by Th41
; verum