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

proof

assume B1: P = [0,1,0] ; :: thesis: rep_pt P = P
then P `3_3 = 0 by MCART_1:def 7;
hence rep_pt P = P by B1, EC_PF_2:def 7; :: thesis: verum

end;

( P `3_3 = 1 implies rep_pt P = P )

proof

assume B1: P `3_3 = 1 ; :: thesis: rep_pt P = P
then (P `3_3) " = 1. (GF p) by EC_PF_2:2;
hence rep_pt P = [((P `1_3) * (1. (GF p))),((P `2_3) * (1. (GF p))),1] by B1, EC_PF_2:def 7
.= P by B1, RECDEF_2:3 ;
:: thesis: verum

end;

hence ( ( P = [0,1,0] or P `3_3 = 1 ) implies rep_pt P = P ) by A1; :: thesis: verum