theorem Th45: :: EC_PF_1:45

for p being Prime
for a, b being Element of (GF p)
for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds
Q in EC_SetProjCo (a,b,p)