set a = z `1 ;
set b = z `2 ;
A1: ( p > 2 + 1 & Disc ((z `1),(z `2),p) <> 0. (GF p) ) by LMZ1Z2;
defpred S₁[ Element of EC_SetProjCo ((z `1),(z `2),p), Element of EC_SetProjCo ((z `1),(z `2),p), set ] means for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( $1 _EQ_ O implies $3 = $2 ) & ( $2 _EQ_ O & not $1 _EQ_ O implies $3 = $1 ) & ( not $1 _EQ_ O & not $2 _EQ_ O & not $1 _EQ_ $2 implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = (($2 `2_3) * ($1 `3_3)) - (($1 `2_3) * ($2 `3_3)) & gf2 = (($2 `1_3) * ($1 `3_3)) - (($1 `1_3) * ($2 `3_3)) & gf3 = ((((gf1 |^ 2) * ($1 `3_3)) * ($2 `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * ($1 `1_3)) * ($2 `3_3)) holds
$3 = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * ($1 `1_3)) * ($2 `3_3)) - gf3)) - (((gf2 |^ 3) * ($1 `2_3)) * ($2 `3_3))),(((gf2 |^ 3) * ($1 `3_3)) * ($2 `3_3))] ) & ( not $1 _EQ_ O & not $2 _EQ_ O & $1 _EQ_ $2 implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * (($1 `3_3) |^ 2)) + (g3 * (($1 `1_3) |^ 2)) & gf2 = ($1 `2_3) * ($1 `3_3) & gf3 = (($1 `1_3) * ($1 `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
$3 = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * (($1 `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) );
A2: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S₁[P,Q,R]

let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis:
consider PP being Element of ProjCo (GF p) such that
B1: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
B2: ( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 ) by B1, ThECSet2;
consider QQ being Element of ProjCo (GF p) such that
B3: ( QQ = Q & QQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
B4: ( QQ `1_3 = Q `1_3 & QQ `2_3 = Q `2_3 & QQ `3_3 = Q `3_3 ) by B3, ThECSet2;
set O = [0,1,0];
reconsider O = [0,1,0] as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
consider OO being Element of ProjCo (GF p) such that
B5: ( OO = O & OO in EC_SetProjCo ((z `1),(z `2),p) ) ;

suppose B6: P _EQ_ O ; :: thesis:

take Q ; :: thesis:
thus S₁[P,Q,Q] by B6; :: thesis:

end;

suppose B6: ( Q _EQ_ O & not P _EQ_ O ) ; :: thesis:

take P ; :: thesis:
thus S₁[P,Q,P] by B6; :: thesis:

end;

suppose B6: ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q ) ; :: thesis:

B7: OO `3_3 = 0 by B5, MCART_1:def 7;
rep_pt PP <> rep_pt OO by B1, B5, B6, ThRepPoint4;
then rep_pt PP <> [0,1,0] by B7, DefRepPoint;
then BB: (rep_pt PP) `3_3 <> 0 by ThRepPoint2;
then B8: P `3_3 <> 0 by B2, ThRepPoint3;
rep_pt QQ <> rep_pt OO by B3, B5, B6, ThRepPoint4;
then rep_pt QQ <> [0,1,0] by B7, DefRepPoint;
then (rep_pt QQ) `3_3 <> 0 by ThRepPoint2;
then B9: Q `3_3 <> 0 by B4, ThRepPoint3;
reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
set gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3));
set gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3));
set gf3 = (((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3));
reconsider gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)), gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)), gf3 = (((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3)) as Element of (GF p) ;
set R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))];
reconsider R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;

per cases ;

suppose C1: P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis:

then (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) by B8, B9, ThECEQ2;
then C2: gf2 = 0. (GF p) by VECTSP_1:19;
then C3: ( gf2 |^ 2 = 0. (GF p) & gf2 |^ 3 = 0. (GF p) ) by ThGF14;
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3) by B6, C1, ThECEQ4;
then gf1 <> 0. (GF p) by VECTSP_1:19;
then C4: gf1 <> 0 by EC_PF_1:11;
then C5: gf1 |^ 2 <> 0 by EC_PF_1:25;
C6: gf3 = (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((0. (GF p)) + (((g2 * (0. (GF p))) * (P `1_3)) * (Q `3_3))) by C3, VECTSP_1:17
.= (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((0. (GF p)) + ((g2 * (0. (GF p))) * ((P `1_3) * (Q `3_3)))) by GROUP_1:def 3
.= (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((0. (GF p)) + ((0. (GF p)) * ((P `1_3) * (Q `3_3)))) by VECTSP_1:6
.= (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((0. (GF p)) + (0. (GF p))) by VECTSP_1:7
.= (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (0. (GF p)) by ALGSTR_1:7
.= ((gf1 |^ 2) * (P `3_3)) * (Q `3_3) by VECTSP_1:18
.= (gf1 |^ 2) * ((P `3_3) * (Q `3_3)) by GROUP_1:def 3 ;
(P `3_3) * (Q `3_3) <> 0 by B8, B9, EC_PF_1:20;
then gf3 <> 0 by C5, C6, EC_PF_1:20;
then gf1 * gf3 <> 0 by C4, EC_PF_1:20;
then C7: gf1 * gf3 <> 0. (GF p) by EC_PF_1:11;
(gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3)) = (gf1 * (((0. (GF p)) * ((P `1_3) * (Q `3_3))) - gf3)) - (((0. (GF p)) * (P `2_3)) * (Q `3_3)) by C3, GROUP_1:def 3
.= (gf1 * (((0. (GF p)) * ((P `1_3) * (Q `3_3))) - gf3)) - ((0. (GF p)) * ((P `2_3) * (Q `3_3))) by GROUP_1:def 3
.= (gf1 * ((0. (GF p)) - gf3)) - ((0. (GF p)) * ((P `2_3) * (Q `3_3))) by VECTSP_1:12
.= (gf1 * ((0. (GF p)) - gf3)) - (0. (GF p)) by VECTSP_1:12
.= gf1 * ((0. (GF p)) - gf3) by VECTSP_1:18
.= gf1 * (- gf3) by VECTSP_1:18
.= - (gf1 * gf3) by VECTSP_1:8 ;
then (gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3)) <> 0. (GF p) by C7, VECTSP_2:3;
then C8: R `2_3 <> 0. (GF p) by MCART_1:def 6;
then R `2_3 <> 0 by EC_PF_1:11;
then R <> [0,0,0] by MCART_1:def 6;
then not R in {[0,0,0]} by TARSKI:def 1;
then R in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by XBOOLE_0:def 5;
then reconsider R = R as Element of ProjCo (GF p) by EC_PF_1:40;
R in EC_SetProjCo ((z `1),(z `2),p)

proof

R `1_3 = gf2 * gf3 by MCART_1:def 5;
then D1: R `1_3 = 0. (GF p) by C2, VECTSP_1:12;
R `3_3 = ((gf2 |^ 3) * (P `3_3)) * (Q `3_3) by MCART_1:def 7
.= (gf2 |^ 3) * ((P `3_3) * (Q `3_3)) by GROUP_1:def 3 ;
then D2: R `3_3 = 0. (GF p) by C3, VECTSP_1:12;
set d = R `2_3 ;
reconsider d = R `2_3 as Element of (GF p) ;
D4: ( OO `1_3 = 0 & OO `2_3 = 1 & OO `3_3 = 0 ) by B5, MCART_1:def 5, MCART_1:def 6, MCART_1:def 7;
D5: d * (OO `1_3) = 0 by D4, EC_PF_1:20
.= R `1_3 by D1, EC_PF_1:11 ;
D6: d * (OO `3_3) = 0 by D4, EC_PF_1:20
.= R `3_3 by D2, EC_PF_1:11 ;
d * (OO `2_3) = d * (1. (GF p)) by D4, EC_PF_1:12
.= R `2_3 by VECTSP_1:def 6 ;
hence R in EC_SetProjCo ((z `1),(z `2),p) by A1, B5, C8, D5, D6, EC_PF_1:45; :: thesis:

end;

then reconsider R = R as Element of EC_SetProjCo ((z `1),(z `2),p) ;
take R ; :: thesis:
thus S₁[P,Q,R] by B6; :: thesis:

end;

suppose not P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis:

then (P `1_3) * (Q `3_3) <> (Q `1_3) * (P `3_3) by B6, B8, B9, ThECEQ2;
then C2: gf2 <> 0. (GF p) by VECTSP_1:19;
then gf2 <> 0 by EC_PF_1:11;
then C3: gf2 |^ 3 <> 0 by EC_PF_1:25;
(P `3_3) * (Q `3_3) <> 0 by B8, B9, EC_PF_1:20;
then (gf2 |^ 3) * ((P `3_3) * (Q `3_3)) <> 0 by C3, EC_PF_1:20;
then (gf2 |^ 3) * ((P `3_3) * (Q `3_3)) <> 0. (GF p) by EC_PF_1:11;
then C5: ((gf2 |^ 3) * (P `3_3)) * (Q `3_3) <> 0. (GF p) by GROUP_1:def 3;
R `3_3 <> 0. (GF p) by C5, MCART_1:def 7;
then R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] by MCART_1:def 7;
then not R in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by TARSKI:def 1;
then R 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 reconsider R = R as Element of ProjCo (GF p) by EC_PF_1:def 6;
gf2 * gf2 <> 0. (GF p) by C2, VECTSP_1:12;
then C8: gf2 |^ 2 <> 0. (GF p) by EC_PF_1:22;
(P `3_3) |^ 2 <> 0 by B2, BB, ThRepPoint3, EC_PF_1:25;
then C9: (P `3_3) |^ 2 <> 0. (GF p) by EC_PF_1:11;
C10: Q `3_3 <> 0. (GF p) by B9, EC_PF_1:11;
(gf2 |^ 2) * ((P `3_3) |^ 2) <> 0. (GF p) by C8, C9, VECTSP_1:12;
then C11: ((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3) <> 0. (GF p) by C10, VECTSP_1:12;
(EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p)

proof

(((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p) by ThAddEllEq5;
then (((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((EC_WEqProjCo ((z `1),(z `2),p)) . R) = 0. (GF p) by EC_PF_1:def 8;
hence (EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p) by C11, VECTSP_1:12; :: thesis:

end;

then R is_on_curve EC_WEqProjCo ((z `1),(z `2),p) by DefOnCurve;
then reconsider R = R as Element of EC_SetProjCo ((z `1),(z `2),p) by ThOnCurve1;
take R ; :: thesis:
thus S₁[P,Q,R] by B6; :: thesis:

end;

suppose B6: ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q ) ; :: thesis:

B7: OO `3_3 = 0 by B5, MCART_1:def 7;
rep_pt PP <> rep_pt OO by B1, B5, B6, ThRepPoint4;
then rep_pt PP <> [0,1,0] by B7, DefRepPoint;
then BB: (rep_pt PP) `3_3 <> 0 by ThRepPoint2;
then B8: P `3_3 <> 0 by B2, ThRepPoint3;
reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g3 = 3 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g4 = 4 mod p as Element of (GF p) by EC_PF_1:14;
reconsider g8 = 8 mod p as Element of (GF p) by EC_PF_1:14;
set gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2));
set gf2 = (P `2_3) * (P `3_3);
set gf3 = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3));
set gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3))));
reconsider gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)), gf2 = (P `2_3) * (P `3_3), gf3 = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)), gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)))) as Element of (GF p) ;
set R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))];
reconsider R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;

per cases ;

suppose C1: P `2_3 = 0 ; :: thesis:

C2: gf2 = 0 by C1, EC_PF_1:20;
then C3: gf3 = 0 by EC_PF_1:20;
C4: gf2 = 0. (GF p) by C2, EC_PF_1:11;
C5: gf3 = 0. (GF p) by C3, EC_PF_1:11;
C6: gf1 <> 0 by B2, BB, C1, ThRepPoint3, ThNonSingular;
then C7: gf1 <> 0. (GF p) by EC_PF_1:11;
gf4 = (gf1 |^ 2) - (0. (GF p)) by C5, VECTSP_1:6
.= gf1 |^ 2 by VECTSP_1:18 ;
then gf4 <> 0 by C6, EC_PF_1:25;
then C8: gf4 <> 0. (GF p) by EC_PF_1:11;
R `2_3 = (gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2)) by MCART_1:def 6
.= (gf1 * ((g4 * (0. (GF p))) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 * gf2)) by C5, EC_PF_1:22
.= (gf1 * ((0. (GF p)) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * ((0. (GF p)) * (0. (GF p)))) by C4, VECTSP_1:12
.= (gf1 * (- gf4)) - ((g8 * ((P `2_3) |^ 2)) * ((0. (GF p)) * (0. (GF p)))) by VECTSP_1:18
.= (gf1 * (- gf4)) - ((g8 * ((P `2_3) |^ 2)) * (0. (GF p))) by VECTSP_1:12
.= (gf1 * (- gf4)) - (0. (GF p)) by VECTSP_1:12
.= gf1 * (- gf4) by VECTSP_1:18
.= - (gf1 * gf4) by VECTSP_1:8 ;
then - (R `2_3) = gf1 * gf4 by RLVECT_1:17;
then - (R `2_3) <> 0. (GF p) by C7, C8, VECTSP_1:12;
then C9: R `2_3 <> 0. (GF p) by VECTSP_2:3;
then R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] by MCART_1:def 6;
then not R in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by TARSKI:def 1;
then R 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 reconsider R = R as Element of ProjCo (GF p) by EC_PF_1:def 6;
R in EC_SetProjCo ((z `1),(z `2),p)

proof

D1: R `1_3 = (g2 * gf4) * gf2 by MCART_1:def 5
.= 0. (GF p) by C4, VECTSP_1:12 ;
D2: gf2 |^ 3 = 0. (GF p) by C2, ThGF14, EC_PF_1:11;
D3: R `3_3 = g8 * (gf2 |^ 3) by MCART_1:def 7
.= 0. (GF p) by D2, VECTSP_1:12 ;
set d = R `2_3 ;
reconsider d = R `2_3 as Element of (GF p) ;
D4: ( OO `1_3 = 0 & OO `2_3 = 1 & OO `3_3 = 0 ) by B5, MCART_1:def 5, MCART_1:def 6, MCART_1:def 7;
D5: d * (OO `1_3) = 0 by D4, EC_PF_1:20
.= R `1_3 by D1, EC_PF_1:11 ;
D6: d * (OO `3_3) = 0 by D4, EC_PF_1:20
.= R `3_3 by D3, EC_PF_1:11 ;
d * (OO `2_3) = d * (1. (GF p)) by D4, EC_PF_1:12
.= R `2_3 by VECTSP_1:def 6 ;
hence R in EC_SetProjCo ((z `1),(z `2),p) by A1, B5, C9, D5, D6, EC_PF_1:45; :: thesis:

end;

then reconsider R = R as Element of EC_SetProjCo ((z `1),(z `2),p) ;
take R ; :: thesis:
thus S₁[P,Q,R] by B6; :: thesis:

end;

suppose C1: P `2_3 <> 0 ; :: thesis:

C2: gf2 <> 0 by B8, C1, EC_PF_1:20;
then gf2 |^ 3 <> 0 by EC_PF_1:25;
then C3: gf2 |^ 3 <> 0. (GF p) by EC_PF_1:11;
C4: g4 = (2 * 2) mod p
.= g2 * g2 by EC_PF_1:18 ;
X: p > 2 by A1, NAT_1:13;
g8 = (4 * 2) mod p
.= g4 * g2 by EC_PF_1:18
.= (g2 |^ 2) * g2 by C4, EC_PF_1:22
.= g2 |^ (2 + 1) by EC_PF_1:24
.= g2 |^ 3 ;
then C5: g8 <> 0. (GF p) by ThGFX, X;
R `3_3 = g8 * (gf2 |^ 3) by MCART_1:def 7;
then R `3_3 <> 0. (GF p) by C3, C5, VECTSP_1:12;
then R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] by MCART_1:def 7;
then not R in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by TARSKI:def 1;
then R 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 reconsider R = R as Element of ProjCo (GF p) by EC_PF_1:def 6;
g4 = g2 |^ 2 by C4, EC_PF_1:22;
then C7: g4 <> 0. (GF p) by ThGFX, X;
gf2 |^ 2 <> 0 by C2, EC_PF_1:25;
then C8: gf2 |^ 2 <> 0. (GF p) by EC_PF_1:11;
(P `3_3) |^ 2 <> 0 by B2, BB, ThRepPoint3, EC_PF_1:25;
then C9: (P `3_3) |^ 2 <> 0. (GF p) by EC_PF_1:11;
g4 * (gf2 |^ 2) <> 0. (GF p) by C7, C8, VECTSP_1:12;
then C10: (g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2) <> 0. (GF p) by C9, VECTSP_1:12;
(EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p)

proof

((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p) by ThDobEllEq5;
then ((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((EC_WEqProjCo ((z `1),(z `2),p)) . R) = 0. (GF p) by EC_PF_1:def 8;
hence (EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p) by C10, VECTSP_1:12; :: thesis:

end;

consider f being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) such that
A3: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S₁[P,Q,f . (P,Q)] from BINOP_1:sch 3(A2);
take f ; :: thesis:
thus for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies f . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies f . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
f . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
f . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) by A3; :: thesis: