let p be Prime; :: thesis: 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); :: thesis: 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); :: thesis: (((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; :: thesis: verum