let p be Prime; :: thesis: for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 <> 0 holds
( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] & P `3_3 <> 0 )
let a, b be Element of (GF p); :: thesis: for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 <> 0 holds
( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] & P `3_3 <> 0 )
let P be Element of ProjCo (GF p); :: thesis: ( (rep_pt P) `3_3 <> 0 implies ( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] & P `3_3 <> 0 ) )
assume A1: (rep_pt P) `3_3 <> 0 ; :: thesis: ( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] & P `3_3 <> 0 )

hereby :: thesis: P `3_3 <> 0

assume A2: rep_pt P <> [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] ; :: thesis: contradiction
rep_pt P = [0,1,0] by A2, Def7;
hence contradiction by A1; :: thesis: verum

end;

assume A3: P `3_3 = 0 ; :: thesis: contradiction
rep_pt P = [0,1,0] by A3, Def7;
hence contradiction by A1; :: thesis: verum