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 _EQ_ Q iff rep_pt P = rep_pt 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 _EQ_ Q iff rep_pt P = rep_pt Q )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P _EQ_ Q iff rep_pt P = rep_pt Q )
set a = z `1 ;
set b = z `2 ;
consider PP being Element of ProjCo (GF p) such that
A1: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
consider QQ being Element of ProjCo (GF p) such that
A2: ( QQ = Q & QQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
set RP = rep_pt PP;
set RQ = rep_pt QQ;

hereby :: thesis: ( rep_pt P = rep_pt Q implies P _EQ_ Q )

assume A3: P _EQ_ Q ; :: thesis: rep_pt P = rep_pt Q
rep_pt PP _EQ_ P by A1, Th36;
then A4: rep_pt PP _EQ_ Q by A3, EC_PF_1:44;
rep_pt QQ _EQ_ Q by A2, Th36;
then rep_pt PP _EQ_ rep_pt QQ by A4, EC_PF_1:44;
then consider a being Element of (GF p) such that
A5: a <> 0. (GF p) and
A6: ( (rep_pt PP) `1_3 = a * ((rep_pt QQ) `1_3) & (rep_pt PP) `2_3 = a * ((rep_pt QQ) `2_3) & (rep_pt PP) `3_3 = a * ((rep_pt QQ) `3_3) ) by EC_PF_1:def 10;

per cases ( PP `3_3 = 0 or PP `3_3 <> 0 ) ;

suppose A7: PP `3_3 = 0 ; :: thesis: rep_pt P = rep_pt Q

then rep_pt PP = [0,1,0] by Def7;
then (rep_pt PP) `3_3 = 0
.= 0. (GF p) by EC_PF_1:11 ;
then (rep_pt QQ) `3_3 = 0. (GF p) by A5, A6, VECTSP_1:12
.= 0 by EC_PF_1:11 ;
then rep_pt QQ = [0,1,0] by Th37;
hence rep_pt P = rep_pt Q by A1, A2, A7, Def7; :: thesis: verum

end;

suppose PP `3_3 <> 0 ; :: thesis: rep_pt P = rep_pt Q

then rep_pt PP = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by Def7;
then A8: (rep_pt PP) `3_3 = 1
.= 1. (GF p) by EC_PF_1:12 ;
then (rep_pt QQ) `3_3 <> 0. (GF p) by A6;
then (rep_pt QQ) `3_3 <> 0 by EC_PF_1:11;
then rep_pt QQ = [((QQ `1_3) * ((QQ `3_3) ")),((QQ `2_3) * ((QQ `3_3) ")),1] by Th38;
then (rep_pt QQ) `3_3 = 1
.= 1. (GF p) by EC_PF_1:12 ;
then a = 1. (GF p) by A6, A8, VECTSP_1:def 8;
then ( (rep_pt PP) `1_3 = (rep_pt QQ) `1_3 & (rep_pt PP) `2_3 = (rep_pt QQ) `2_3 & (rep_pt PP) `3_3 = (rep_pt QQ) `3_3 ) by A6, VECTSP_1:def 8;
then rep_pt PP = [((rep_pt QQ) `1_3),((rep_pt QQ) `2_3),((rep_pt QQ) `3_3)] by AA
.= rep_pt QQ by AA ;
hence rep_pt P = rep_pt Q by A1, A2; :: thesis: verum

end;

end;

end;

assume A9: rep_pt P = rep_pt Q ; :: thesis: P _EQ_ Q
A10: rep_pt QQ _EQ_ P by A2, A9, Th36;
rep_pt QQ _EQ_ Q by A2, Th36;
hence P _EQ_ Q by A10, EC_PF_1:44; :: thesis: verum