let p be Prime; :: thesis: for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3 = 1 )
let a, b be Element of (GF p); :: thesis: for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3 = 1 )
let P be Element of ProjCo (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3 <> 0 implies ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3 = 1 ) )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3 <> 0 ) ; :: thesis: ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3 = 1 )
set d = (P `3) " ;
AS0: P `3 <> 0. (GF p) by AS, XLm2;
AS1: (P `3) " <> 0. (GF p)

proof

assume A1: (P `3) " = 0. (GF p) ; :: thesis: contradiction
A2: ((P `3) ") * (P `3) = 1_ (GF p) by AS0, VECTSP_1:def 10
.= 1 by XLm3 ;
((P `3) ") * (P `3) = 0. (GF p) by A1, VECTSP_1:12
.= 0 by XLm2 ;
hence contradiction by A2; :: thesis: verum

end;

reconsider Q = [(((P `3) ") * (P `1)),(((P `3) ") * (P `2)),(((P `3) ") * (P `3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
P1: ( Q `1 = ((P `3) ") * (P `1) & Q `2 = ((P `3) ") * (P `2) & Q `3 = ((P `3) ") * (P `3) ) by MCART_1:43;
then Q in EC_SetProjCo (a,b,p) by AS, AS1, LmEQV4;
then consider PP being Element of ProjCo (GF p) such that
P2: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ;
reconsider Q = Q as Element of ProjCo (GF p) by P2;
take Q ; :: thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3 = 1 )
thus Q in EC_SetProjCo (a,b,p) by P1, AS, AS1, LmEQV4; :: thesis: ( Q _EQ_ P & Q `3 = 1 )
thus Q _EQ_ P by P1, AS1, DefEQV; :: thesis: Q `3 = 1
thus Q `3 = ((P `3) ") * (P `3) by MCART_1:def 7
.= 1_ (GF p) by AS0, VECTSP_1:def 10
.= 1 by XLm3 ; :: thesis: verum