let p be Prime; for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)
let a, b be Element of (GF p); for P being Element of EC_SetProjCo (a,b,p) holds (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)
let P be Element of EC_SetProjCo (a,b,p); (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)
consider PP being Element of ProjCo (GF p) such that
A1:
( PP = P & PP in EC_SetProjCo (a,b,p) )
;
A2:
( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 )
by A1, Th32;
P is_on_curve EC_WEqProjCo (a,b,p)
by Th34;
hence
(((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)
by A2, EC_PF_1:def 8, A1; verum