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)

for a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds

P _EQ_ Q

let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)

for a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds

P _EQ_ Q

let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: for a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds

P _EQ_ Q

let a be Element of (GF p); :: thesis: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) implies P _EQ_ Q )

assume that

A1: a <> 0. (GF p) and

A2: ( P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ; :: thesis: P _EQ_ Q

reconsider PP = P, QQ = Q as Element of ProjCo (GF p) ;

A3: PP `1_3 = a * (Q `1_3) by A2, EC_PF_2:32

.= a * (QQ `1_3) by EC_PF_2:32 ;

A4: PP `2_3 = a * (Q `2_3) by A2, EC_PF_2:32

.= a * (QQ `2_3) by EC_PF_2:32 ;

PP `3_3 = a * (Q `3_3) by A2, EC_PF_2:32

.= a * (QQ `3_3) by EC_PF_2:32 ;

hence P _EQ_ Q by A1, A3, A4, EC_PF_1:def 10; :: thesis: verum

for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)

for a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds

P _EQ_ Q

let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)

for a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds

P _EQ_ Q

let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: for a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds

P _EQ_ Q

let a be Element of (GF p); :: thesis: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) implies P _EQ_ Q )

assume that

A1: a <> 0. (GF p) and

A2: ( P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ; :: thesis: P _EQ_ Q

reconsider PP = P, QQ = Q as Element of ProjCo (GF p) ;

A3: PP `1_3 = a * (Q `1_3) by A2, EC_PF_2:32

.= a * (QQ `1_3) by EC_PF_2:32 ;

A4: PP `2_3 = a * (Q `2_3) by A2, EC_PF_2:32

.= a * (QQ `2_3) by EC_PF_2:32 ;

PP `3_3 = a * (Q `3_3) by A2, EC_PF_2:32

.= a * (QQ `3_3) by EC_PF_2:32 ;

hence P _EQ_ Q by A1, A3, A4, EC_PF_1:def 10; :: thesis: verum