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_3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_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_3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_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_3 <> 0 implies ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 ) ; :: thesis: ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
set d = (P `3_3) " ;
A2: P `3_3 <> 0. (GF p) by A1, Th11;
A3: (P `3_3) " <> 0. (GF p)

proof

assume A4: (P `3_3) " = 0. (GF p) ; :: thesis: contradiction
A5: ((P `3_3) ") * (P `3_3) = 1_ (GF p) by A2, VECTSP_1:def 10
.= 1 by Th12 ;
((P `3_3) ") * (P `3_3) = 0. (GF p) by A4
.= 0 by Th11 ;
hence contradiction by A5; :: thesis: verum

end;

reconsider Q = [(((P `3_3) ") * (P `1_3)),(((P `3_3) ") * (P `2_3)),(((P `3_3) ") * (P `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
A6: ( Q `1_3 = ((P `3_3) ") * (P `1_3) & Q `2_3 = ((P `3_3) ") * (P `2_3) & Q `3_3 = ((P `3_3) ") * (P `3_3) ) ;
then Q in EC_SetProjCo (a,b,p) by A1, A3, Th45;
then consider PP being Element of ProjCo (GF p) such that
A7: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ;
reconsider Q = Q as Element of ProjCo (GF p) by A7;
take Q ; :: thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )
thus Q in EC_SetProjCo (a,b,p) by A6, A1, A3, Th45; :: thesis: ( Q _EQ_ P & Q `3_3 = 1 )
thus Q _EQ_ P by A3; :: thesis: Q `3_3 = 1
thus Q `3_3 = ((P `3_3) ") * (P `3_3)
.= 1_ (GF p) by A2, VECTSP_1:def 10
.= 1 by Th12 ; :: thesis: verum