set a = z `1 ;
set b = z `2 ;
A1: ( p > 2 + 1 & Disc ((z `1),(z `2),p) <> 0. (GF p) ) by Th30;
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
A3: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A4: ( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 ) by A3, Th32;
consider QQ being Element of ProjCo (GF p) such that
A5: ( QQ = Q & QQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
A6: ( QQ `1_3 = Q `1_3 & QQ `2_3 = Q `2_3 & QQ `3_3 = Q `3_3 ) by A5, Th32;
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
A7: ( OO = O & OO in EC_SetProjCo ((z `1),(z `2),p) ) ;

suppose A8: P _EQ_ O ; :: thesis:

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

end;

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

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

end;

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

A11: OO `3_3 = 0 by A7;
rep_pt PP <> rep_pt OO by A3, A7, A10, Th39;
then rep_pt PP <> [0,1,0] by A11, Def7;
then A12: (rep_pt PP) `3_3 <> 0 by Th37;
then A13: P `3_3 <> 0 by A4, Th38;
rep_pt QQ <> rep_pt OO by A5, A7, A10, Th39;
then rep_pt QQ <> [0,1,0] by A11, Def7;
then (rep_pt QQ) `3_3 <> 0 by Th37;
then A14: Q `3_3 <> 0 by A6, Th38;
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 A15: P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis:

then (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) by A13, A14, Th50;
then A16: gf2 = 0. (GF p) by VECTSP_1:19;
then A17: ( gf2 |^ 2 = 0. (GF p) & gf2 |^ 3 = 0. (GF p) ) by Th5;
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3) by A10, A15, Th52;
then gf1 <> 0. (GF p) by VECTSP_1:19;
then A18: gf1 <> 0 by EC_PF_1:11;
then A19: gf1 |^ 2 <> 0 by EC_PF_1:25;
A20: gf3 = (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((0. (GF p)) + (((g2 * (0. (GF p))) * (P `1_3)) * (Q `3_3))) by A17, VECTSP_1:17
.= (((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 A13, A14, EC_PF_1:20;
then gf3 <> 0 by A19, A20, EC_PF_1:20;
then gf1 * gf3 <> 0 by A18, EC_PF_1:20;
then A21: 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 A17
.= 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 A21, VECTSP_2:3;
then A22: R `2_3 <> 0. (GF p) ;
then R <> [0,0,0] by EC_PF_1:11;
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

A23: R `1_3 = 0. (GF p) by A16;
A24: R `3_3 = 0. (GF p) by A17;
set d = R `2_3 ;
reconsider d = R `2_3 as Element of (GF p) ;
A25: ( OO `1_3 = 0 & OO `2_3 = 1 & OO `3_3 = 0 ) by A7;
A26: d * (OO `1_3) = 0 by A25, EC_PF_1:20
.= R `1_3 by A23, EC_PF_1:11 ;
A27: d * (OO `3_3) = 0 by A25, EC_PF_1:20
.= R `3_3 by A24, EC_PF_1:11 ;
d * (OO `2_3) = d * (1. (GF p)) by A25, EC_PF_1:12
.= R `2_3 ;
hence R in EC_SetProjCo ((z `1),(z `2),p) by A1, A7, A22, A26, A27, 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 A10; :: 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 A10, A13, A14, Th50;
then A28: gf2 <> 0. (GF p) by VECTSP_1:19;
then gf2 <> 0 by EC_PF_1:11;
then A29: gf2 |^ 3 <> 0 by EC_PF_1:25;
(P `3_3) * (Q `3_3) <> 0 by A13, A14, EC_PF_1:20;
then (gf2 |^ 3) * ((P `3_3) * (Q `3_3)) <> 0 by A29, EC_PF_1:20;
then (gf2 |^ 3) * ((P `3_3) * (Q `3_3)) <> 0. (GF p) by EC_PF_1:11;
then A30: ((gf2 |^ 3) * (P `3_3)) * (Q `3_3) <> 0. (GF p) by GROUP_1:def 3;
R `3_3 <> 0. (GF p) by A30;
then R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] ;
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 A28, VECTSP_1:12;
then A31: gf2 |^ 2 <> 0. (GF p) by EC_PF_1:22;
(P `3_3) |^ 2 <> 0 by A4, A12, Th38, EC_PF_1:25;
then A32: (P `3_3) |^ 2 <> 0. (GF p) by EC_PF_1:11;
A33: Q `3_3 <> 0. (GF p) by A14, EC_PF_1:11;
(gf2 |^ 2) * ((P `3_3) |^ 2) <> 0. (GF p) by A31, A32, VECTSP_1:12;
then A34: ((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3) <> 0. (GF p) by A33, 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 Th58;
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 A34, VECTSP_1:12; :: thesis:

end;

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

end;

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

A36: OO `3_3 = 0 by A7;
rep_pt PP <> rep_pt OO by A3, A7, A35, Th39;
then rep_pt PP <> [0,1,0] by A36, Def7;
then A37: (rep_pt PP) `3_3 <> 0 by Th37;
then A38: P `3_3 <> 0 by A4, Th38;
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 A39: P `2_3 = 0 ; :: thesis:

A40: gf2 = 0 by A39, EC_PF_1:20;
then A41: gf3 = 0 by EC_PF_1:20;
A42: gf2 = 0. (GF p) by A40, EC_PF_1:11;
A43: gf3 = 0. (GF p) by A41, EC_PF_1:11;
A44: gf1 <> 0 by A4, A37, A39, Th38, Th53;
then A45: gf1 <> 0. (GF p) by EC_PF_1:11;
gf4 = (gf1 |^ 2) - (0. (GF p)) by A43
.= gf1 |^ 2 by VECTSP_1:18 ;
then gf4 <> 0 by A44, EC_PF_1:25;
then A46: gf4 <> 0. (GF p) by EC_PF_1:11;
R `2_3 = (gf1 * ((g4 * (0. (GF p))) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 * gf2)) by A43, EC_PF_1:22
.= (gf1 * (- gf4)) - ((g8 * ((P `2_3) |^ 2)) * ((0. (GF p)) * (0. (GF p)))) by VECTSP_1:18, A42
.= 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 A45, A46, VECTSP_1:12;
then A47: R `2_3 <> 0. (GF p) by VECTSP_2:3;
then R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] ;
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

A48: R `1_3 = 0. (GF p) by A42;
0 = 0. (GF p) by EC_PF_1:11;
then A49: gf2 |^ 3 = 0. (GF p) by A40, Th5;
A50: R `3_3 = 0. (GF p) by A49;
set d = R `2_3 ;
reconsider d = R `2_3 as Element of (GF p) ;
A51: ( OO `1_3 = 0 & OO `2_3 = 1 & OO `3_3 = 0 ) by A7;
A52: d * (OO `1_3) = 0 by A51, EC_PF_1:20
.= R `1_3 by A48, EC_PF_1:11 ;
A53: d * (OO `3_3) = 0 by A51, EC_PF_1:20
.= R `3_3 by A50, EC_PF_1:11 ;
d * (OO `2_3) = d * (1. (GF p)) by A51, EC_PF_1:12
.= R `2_3 ;
hence R in EC_SetProjCo ((z `1),(z `2),p) by A1, A7, A47, A52, A53, 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 A35; :: thesis:

end;

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

A55: gf2 <> 0 by A38, A54, EC_PF_1:20;
then gf2 |^ 3 <> 0 by EC_PF_1:25;
then A56: gf2 |^ 3 <> 0. (GF p) by EC_PF_1:11;
A57: g4 = (2 * 2) mod p
.= g2 * g2 by EC_PF_1:18 ;
A58: p > 2 by A1, NAT_1:13;
g8 = (4 * 2) mod p
.= g4 * g2 by EC_PF_1:18
.= (g2 |^ 2) * g2 by A57, EC_PF_1:22
.= g2 |^ (2 + 1) by EC_PF_1:24
.= g2 |^ 3 ;
then A59: g8 <> 0. (GF p) by Th28, A58;
R `3_3 <> 0. (GF p) by A56, A59, VECTSP_1:12;
then R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] ;
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 A57, EC_PF_1:22;
then A60: g4 <> 0. (GF p) by Th28, A58;
gf2 |^ 2 <> 0 by A55, EC_PF_1:25;
then A61: gf2 |^ 2 <> 0. (GF p) by EC_PF_1:11;
(P `3_3) |^ 2 <> 0 by A4, A37, Th38, EC_PF_1:25;
then A62: (P `3_3) |^ 2 <> 0. (GF p) by EC_PF_1:11;
g4 * (gf2 |^ 2) <> 0. (GF p) by A60, A61, VECTSP_1:12;
then A63: (g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2) <> 0. (GF p) by A62, 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 Th63;
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 A63, VECTSP_1:12; :: thesis:

end;

then R is_on_curve EC_WEqProjCo ((z `1),(z `2),p) ;
then reconsider R = R as Element of EC_SetProjCo ((z `1),(z `2),p) by Th34;
take R ; :: thesis:
thus S₁[P,Q,R] by A35; :: 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
A64: 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 A64; :: thesis: