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) holds
( P = Q iff (compell_ProjCo (z,p)) . P = (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) 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); :: thesis: ( 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 ) ; :: thesis: ( (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 ; :: thesis: P = Q
thus P = (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . Q) by A1, Th41
.= Q by Th41 ; :: thesis: verum