let p be Prime; :: thesis: for a, b, d1, Y1, d2, Y2 being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) holds
( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) )
let a, b, d1, Y1, d2, Y2 be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) implies ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) ) ; :: thesis: ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) )
hereby :: thesis: ( d1 = d2 & Y1 = Y2 implies Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) )
assume Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) ; :: thesis: ( d2 = d1 & Y2 = Y1 )
then [d2,Y2,1] in Class ((R_EllCur (a,b,p)),[d1,Y1,1]) by A1, EQREL_1:23;
then A2: [[d1,Y1,1],[d2,Y2,1]] in R_EllCur (a,b,p) by EQREL_1:18;
reconsider P = [d1,Y1,1], Q = [d2,Y2,1] as Element of ProjCo (GF p) by A1;
P _EQ_ Q by Th47, A1, A2;
then consider a being Element of (GF p) such that
A3: ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) by Def10;
A4: p > 1 by INT_2:def 4;
A5: 1. (GF p) = 1 by A4, INT_3:14
.= P `3_3 ;
A6: 1. (GF p) = 1 by A4, INT_3:14
.= a * (P `3_3) by A3
.= a by A5 ;
thus d2 = a * (P `1_3) by A3
.= P `1_3 by A6
.= d1 ; :: thesis: Y2 = Y1
thus Y2 = a * (P `2_3) by A3
.= P `2_3 by A6
.= Y1 ; :: thesis: verum
end;
assume ( d1 = d2 & Y1 = Y2 ) ; :: thesis: Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1])
hence Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) ; :: thesis: verum