per cases ( P `3_3 <> 0 or P `3_3 = 0 ) ;

suppose A1: P `3_3 <> 0 ; :: thesis: ( ( P `3_3 <> 0 implies [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] is Element of ProjCo (GF p) ) & ( P `3_3 = 0 implies [0,1,0] is Element of ProjCo (GF p) ) )

[((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),(1. (GF p))] <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] by XTUPLE_0:3;
then not [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),(1. (GF p))] in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by TARSKI:def 1;
then [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),(1. (GF p))] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by XBOOLE_0:def 5;
then [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),(1. (GF p))] in ProjCo (GF p) by EC_PF_1:def 6;
hence ( ( P `3_3 <> 0 implies [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] is Element of ProjCo (GF p) ) & ( P `3_3 = 0 implies [0,1,0] is Element of ProjCo (GF p) ) ) by A1, EC_PF_1:12; :: thesis: verum

end;

suppose A2: P `3_3 = 0 ; :: thesis: ( ( P `3_3 <> 0 implies [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] is Element of ProjCo (GF p) ) & ( P `3_3 = 0 implies [0,1,0] is Element of ProjCo (GF p) ) )

set Q = [0,1,0];
thus ( ( P `3_3 <> 0 implies [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] is Element of ProjCo (GF p) ) & ( P `3_3 = 0 implies [0,1,0] is Element of ProjCo (GF p) ) ) by A2, EC_PF_1:42; :: thesis: verum

end;

end;