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 )

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

( P `3_3 = 1 implies rep_pt P = P )
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;then P `3_3 = 0 by MCART_1:def 7;

hence rep_pt P = P by B1, EC_PF_2:def 7; :: thesis: verum

proof

hence
( ( P = [0,1,0] or P `3_3 = 1 ) implies rep_pt P = P )
by A1; :: thesis: verum
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;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