:: Operations of Points on Elliptic Curve in Projective Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received November 3, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

theorem ThGF10: :: EC_PF_2:1
for K being Field
for a1, a2 being Element of K st a1 = - a2 holds
a1 |^ 2 = a2 |^ 2
proofend;

theorem :: EC_PF_2:2
for K being Field holds (1. K) " = 1. K
proofend;

theorem ThGF12: :: EC_PF_2:3
for K being Field
for a2, a4, a1, a3 being Element of K st a2 <> 0. K &amp; a4 <> 0. K &amp; a1 * (a2 ") = a3 * (a4 ") holds
a1 * a4 = a2 * a3
proofend;

theorem ThGF13: :: EC_PF_2:4
for K being Field
for a2, a4, a1, a3 being Element of K st a2 <> 0. K &amp; a4 <> 0. K &amp; a1 * a4 = a2 * a3 holds
a1 * (a2 ") = a3 * (a4 ")
proofend;

theorem ThGF14: :: EC_PF_2:5
for n being Nat
for K being Field
for a1 being Element of K st a1 = 0. K &amp; n > 1 holds
a1 |^ n = 0. K
proofend;

theorem :: EC_PF_2:6
for K being Field
for a1, a2 being Element of K st a1 = - a2 holds
- a1 = a2
proofend;

theorem ThGF001: :: EC_PF_2:7
for K being Field
for a1, a2, a3, a4 being Element of K holds
( ((a1 + a2) + a3) + a4 = ((a4 + a2) + a3) + a1 &amp; ((a1 + a2) + a3) + a4 = ((a1 + a4) + a3) + a2 )
proofend;

theorem ThGF002: :: EC_PF_2:8
for K being Field
for a1, a2, a3, a4, a5 being Element of K holds
( ((a1 + a2) + a3) + a4 = a1 + ((a2 + a3) + a4) &amp; (((a1 + a2) + a3) + a4) + a5 = a1 + (((a2 + a3) + a4) + a5) )
proofend;

theorem :: EC_PF_2:9
for K being Field
for a1, a2, a3, a4, a5, a6 being Element of K holds ((((a1 + a2) + a3) + a4) + a5) + a6 = a1 + ((((a2 + a3) + a4) + a5) + a6)
proofend;

theorem ThGF101: :: EC_PF_2:10
for K being Field
for a1, a2, a3, a4 being Element of K holds
( ((a1 * a2) * a3) * a4 = ((a4 * a2) * a3) * a1 &amp; ((a1 * a2) * a3) * a4 = ((a1 * a4) * a3) * a2 )
proofend;

theorem ThGF102: :: EC_PF_2:11
for K being Field
for a1, a2, a3, a4, a5 being Element of K holds
( ((a1 * a2) * a3) * a4 = a1 * ((a2 * a3) * a4) &amp; (((a1 * a2) * a3) * a4) * a5 = a1 * (((a2 * a3) * a4) * a5) )
proofend;

theorem ThGF103: :: EC_PF_2:12
for K being Field
for a1, a2, a3, a4, a5, a6 being Element of K holds
( ((((a1 * a2) * a3) * a4) * a5) * a6 = a1 * ((((a2 * a3) * a4) * a5) * a6) &amp; ((((a1 * a2) * a3) * a4) * a5) * a6 = ((a1 * ((a2 * a3) * a4)) * a5) * a6 )
proofend;

theorem ThGF200: :: EC_PF_2:13
for n being Nat
for K being Field
for a1, a2, a3 being Element of K holds ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
proofend;

theorem ThGF300: :: EC_PF_2:14
for K being Field
for a1, a2, a3, a4 being Element of K holds
( a1 * ((a2 + a3) + a4) = ((a1 * a2) + (a1 * a3)) + (a1 * a4) &amp; a1 * ((a2 + a3) - a4) = ((a1 * a2) + (a1 * a3)) - (a1 * a4) &amp; a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) &amp; a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) &amp; a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) &amp; a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) &amp; a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) &amp; a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
proofend;

theorem ThGFA3: :: EC_PF_2:15
for K being Field
for a1, a2 being Element of K holds (a1 + a2) * (a1 - a2) = (a1 |^ 2) - (a2 |^ 2)
proofend;

theorem :: EC_PF_2:16
for K being Field
for a1, a2 being Element of K holds (a1 + a2) * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) + (a2 |^ 3)
proofend;

theorem ThGFA5: :: EC_PF_2:17
for K being Field
for a1, a2 being Element of K holds (a1 - a2) * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) - (a2 |^ 3)
proofend;

definition
let n, p be natural number ;
attrp is n _or_greater  means :Defgt3: :: EC_PF_2:def 1
n <= p;
end;

:: deftheorem Defgt3 defines _or_greater EC_PF_2:def_1_:_
 for n, p being natural number holds
( p is n _or_greater iff n <= p );

registration
cluster epsilon-transitive epsilon-connected ordinal natural V11() V12() integer prime ext-real 5 _or_greater for set ;
existence
 ex b1 being natural number st
( b1 is 5 _or_greater &amp; b1 is prime )
proofend;
end;

theorem ThGF3: :: EC_PF_2:18
for i, j being Integer
for p being Prime
for gi, gj, gij, a being Element of (GF p) st gi = i mod p &amp; gj = j mod p &amp; gij = (i + j) mod p holds
(gi * a) + (gj * a) = gij * a
proofend;

theorem ThGF4: :: EC_PF_2:19
for i, j being Integer
for p being Prime
for gi, gj, a being Element of (GF p) st gi = i mod p &amp; gj = j mod p &amp; j = i + 1 holds
(gi * a) + a = gj * a
proofend;

theorem ThGF5: :: EC_PF_2:20
for p being Prime
for g2, a being Element of (GF p) st g2 = 2 mod p holds
a + a = g2 * a
proofend;

theorem ThGF6: :: EC_PF_2:21
for i, j being Integer
for p being Prime
for gi, gj, gij, a being Element of (GF p) st gi = i mod p &amp; gj = j mod p &amp; gij = (i - j) mod p holds
(gi * a) - (gj * a) = gij * a
proofend;

theorem ThGF7: :: EC_PF_2:22
for i, j being Integer
for p being Prime
for gi, gj, a being Element of (GF p) st gi = i mod p &amp; gj = j mod p &amp; i = j + 1 holds
(gi * a) - (gj * a) = a
proofend;

theorem ThGF8: :: EC_PF_2:23
for i, j being Integer
for p being Prime
for gi, gj, a being Element of (GF p) st gi = i mod p &amp; gj = j mod p &amp; i = j + 1 holds
(gi * a) - a = gj * a
proofend;

theorem ThGF9: :: EC_PF_2:24
for p being Prime
for g2, a being Element of (GF p) st g2 = 2 mod p holds
(g2 * a) - a = a
proofend;

theorem ThGFA1: :: EC_PF_2:25
for p being Prime
for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a + b) |^ 2 = ((a |^ 2) + ((g2 * a) * b)) + (b |^ 2)
proofend;

theorem ThGFA2: :: EC_PF_2:26
for p being Prime
for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a - b) |^ 2 = ((a |^ 2) - ((g2 * a) * b)) + (b |^ 2)
proofend;

theorem ThGFA6: :: EC_PF_2:27
for p being Prime
for g2, a, b, c, d being Element of (GF p) st g2 = 2 mod p holds
((a * c) + (b * d)) |^ 2 = (((a |^ 2) * (c |^ 2)) + ((((g2 * a) * b) * c) * d)) + ((b |^ 2) * (d |^ 2))
proofend;

theorem ThGFX: :: EC_PF_2:28
for p being Prime
for n being Nat
for g2 being Element of (GF p) st p > 2 &amp; g2 = 2 mod p holds
( g2 <> 0. (GF p) &amp; g2 |^ n <> 0. (GF p) )
proofend;

theorem :: EC_PF_2:29
for p being Prime
for n being Nat
for g2, g3 being Element of (GF p) st p > 3 &amp; g3 = 3 mod p holds
( g3 <> 0. (GF p) &amp; g3 |^ n <> 0. (GF p) )
proofend;

begin

definition
let p be 5 _or_greater Prime;
func EC_WParam p ->  Subset of [: the carrier of (GF p), the carrier of (GF p):] equals :: EC_PF_2:def 2
 {  [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p)  }  ;
correctness
coherence
{  [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p)  }  is Subset of [: the carrier of (GF p), the carrier of (GF p):];
proofend;
end;

:: deftheorem  defines EC_WParam EC_PF_2:def_2_:_
 for p being 5 _or_greater Prime holds EC_WParam p =  {  [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p)  }  ;

registration
let p be 5 _or_greater Prime;
cluster EC_WParam p ->  non empty ;
coherence
 not EC_WParam p is empty
proofend;
end;

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
:: original:`1
redefine funcz `1  ->  Element of (GF p);
correctness
coherence
z `1 is Element of (GF p);
proofend;
:: original:`2
redefine funcz `2  ->  Element of (GF p);
correctness
coherence
z `2 is Element of (GF p);
proofend;
end;

theorem LMZ1Z2: :: EC_PF_2:30
for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds
( p > 3 &amp; Disc ((z `1),(z `2),p) <> 0. (GF p) )
proofend;

definition
let p be Prime;
let a, b be Element of (GF p);
let P be Element of EC_SetProjCo (a,b,p);
funcP `1_3  ->  Element of (GF p) means :DefX: :: EC_PF_2:def 3
 for px, py, pz being set st P = [px,py,pz] holds
it = px;
existence
 ex b1 being Element of (GF p) st
for px, py, pz being set st P = [px,py,pz] holds
b1 = px
proofend;
uniqueness
 for b1, b2 being Element of (GF p) st ( for px, py, pz being set st P = [px,py,pz] holds
b1 = px ) &amp; ( for px, py, pz being set st P = [px,py,pz] holds
b2 = px ) holds
b1 = b2
proofend;
funcP `2_3  ->  Element of (GF p) means :DefY: :: EC_PF_2:def 4
 for px, py, pz being set st P = [px,py,pz] holds
it = py;
existence
 ex b1 being Element of (GF p) st
for px, py, pz being set st P = [px,py,pz] holds
b1 = py
proofend;
uniqueness
 for b1, b2 being Element of (GF p) st ( for px, py, pz being set st P = [px,py,pz] holds
b1 = py ) &amp; ( for px, py, pz being set st P = [px,py,pz] holds
b2 = py ) holds
b1 = b2
proofend;
funcP `3_3  ->  Element of (GF p) means :DefZ: :: EC_PF_2:def 5
 for px, py, pz being set st P = [px,py,pz] holds
it = pz;
existence
 ex b1 being Element of (GF p) st
for px, py, pz being set st P = [px,py,pz] holds
b1 = pz
proofend;
uniqueness
 for b1, b2 being Element of (GF p) st ( for px, py, pz being set st P = [px,py,pz] holds
b1 = pz ) &amp; ( for px, py, pz being set st P = [px,py,pz] holds
b2 = pz ) holds
b1 = b2
proofend;
end;

:: deftheorem DefX defines `1_3 EC_PF_2:def_3_:_
 for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b5 being Element of (GF p) holds
( b5 = P `1_3 iff for px, py, pz being set st P = [px,py,pz] holds
b5 = px );

:: deftheorem DefY defines `2_3 EC_PF_2:def_4_:_
 for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b5 being Element of (GF p) holds
( b5 = P `2_3 iff for px, py, pz being set st P = [px,py,pz] holds
b5 = py );

:: deftheorem DefZ defines `3_3 EC_PF_2:def_5_:_
 for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b5 being Element of (GF p) holds
( b5 = P `3_3 iff for px, py, pz being set st P = [px,py,pz] holds
b5 = pz );

theorem ThECSet1: :: EC_PF_2:31
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds P = [(P `1_3),(P `2_3),(P `3_3)]
proofend;

theorem ThECSet2: :: EC_PF_2:32
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for Q being Element of ProjCo (GF p) holds
( P = Q iff ( P `1_3 = Q `1_3 &amp; P `2_3 = Q `2_3 &amp; P `3_3 = Q `3_3 ) )
proofend;

theorem :: EC_PF_2:33
for p being Prime
for a, b, Px, Py, Pz being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) st P = [Px,Py,Pz] holds
( P `1_3 = Px &amp; P `2_3 = Py &amp; P `3_3 = Pz ) by DefX, DefY, DefZ;

definition
let p be Prime;
let P be Element of ProjCo (GF p);
let CEQ be Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p);
predP is_on_curve CEQ means :DefOnCurve: :: EC_PF_2:def 6
CEQ . P = 0. (GF p);
correctness
;
end;

:: deftheorem DefOnCurve defines is_on_curve EC_PF_2:def_6_:_
 for p being Prime
for P being Element of ProjCo (GF p)
for CEQ being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds
( P is_on_curve CEQ iff CEQ . P = 0. (GF p) );

theorem ThOnCurve1: :: EC_PF_2:34
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) holds
( P is_on_curve EC_WEqProjCo (a,b,p) iff P is Element of EC_SetProjCo (a,b,p) )
proofend;

theorem ThOnCurve2: :: EC_PF_2:35
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)
proofend;

definition
let p be Prime;
let P be Element of ProjCo (GF p);
func rep_pt P ->  Element of ProjCo (GF p) equals :DefRepPoint: :: EC_PF_2:def 7
[((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] if P `3_3 <> 0
[0,1,0] if P `3_3 = 0
;
coherence
 ( ( P `3_3 <> 0 implies [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] is Element of ProjCo (GF p) ) &amp; ( P `3_3 = 0 implies [0,1,0] is Element of ProjCo (GF p) ) )
proofend;
consistency
 for b1 being Element of ProjCo (GF p) st P `3_3 <> 0 &amp; P `3_3 = 0 holds
( b1 = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] iff b1 = [0,1,0] ) ;
end;

:: deftheorem DefRepPoint defines rep_pt EC_PF_2:def_7_:_
 for p being Prime
for P being Element of ProjCo (GF p) holds
( ( P `3_3 <> 0 implies rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] ) &amp; ( P `3_3 = 0 implies rep_pt P = [0,1,0] ) );

theorem ThRepPoint1: :: EC_PF_2:36
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( rep_pt P _EQ_ P &amp; rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )
proofend;

theorem ThRepPoint2: :: EC_PF_2:37
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 = 0 holds
( rep_pt P = [0,1,0] &amp; P `3_3 = 0 )
proofend;

theorem ThRepPoint3: :: EC_PF_2:38
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 <> 0 holds
( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] &amp; P `3_3 <> 0 )
proofend;

theorem ThRepPoint4: :: EC_PF_2:39
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P _EQ_ Q iff rep_pt P = rep_pt Q )
proofend;

begin

LmCOMPELL:  for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds [(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p)
proofend;

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
func compell_ProjCo (z,p) ->  Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) means :DefCompEll: :: EC_PF_2:def 8
 for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds it . P = [(P `1_3),(- (P `2_3)),(P `3_3)];
existence
 ex b1 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) st
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b1 . P = [(P `1_3),(- (P `2_3)),(P `3_3)]
proofend;
uniqueness
 for b1, b2 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) st ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b1 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) &amp; ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b2 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) holds
b1 = b2
proofend;
end;

:: deftheorem DefCompEll defines compell_ProjCo EC_PF_2:def_8_:_
 for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b3 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) holds
( b3 = compell_ProjCo (z,p) iff for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b3 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] );

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
let F be Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p));
let P be Element of EC_SetProjCo ((z `1),(z `2),p);
:: original:.
redefine funcF . P ->  Element of EC_SetProjCo ((z `1),(z `2),p);
correctness
coherence
F . P is Element of EC_SetProjCo ((z `1),(z `2),p);
proofend;
end;

theorem ThCOMPELL0: :: EC_PF_2:40
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(compell_ProjCo (z,p)) . O _EQ_ O
proofend;

theorem ThCOMPELL1: :: EC_PF_2:41
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = P
proofend;

theorem ThCOMPELL2: :: EC_PF_2:42
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P)
proofend;

theorem ThCOMPELL3: :: EC_PF_2:43
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P = Q iff (compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q )
proofend;

theorem ThCOMPELL4: :: EC_PF_2:44
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
( P _EQ_ (compell_ProjCo (z,p)) . P iff P `2_3 = 0 )
proofend;

theorem ThCOMPELL5: :: EC_PF_2:45
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
( ( P `1_3 = Q `1_3 &amp; P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
proofend;

theorem ThEQCOMP1: :: EC_PF_2:46
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P _EQ_ Q iff (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q )
proofend;

theorem ThEQCOMP2: :: EC_PF_2:47
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P _EQ_ (compell_ProjCo (z,p)) . Q iff (compell_ProjCo (z,p)) . P _EQ_ Q )
proofend;

theorem ThEQCOMP3: :: EC_PF_2:48
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 &amp; Q `3_3 <> 0 holds
( rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) iff P _EQ_ (compell_ProjCo (z,p)) . Q )
proofend;

theorem :: EC_PF_2:49
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P _EQ_ Q holds
(P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
proofend;

theorem ThECEQ2: :: EC_PF_2:50
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 &amp; Q `3_3 <> 0 holds
( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) )
proofend;

theorem ThECEQ3: :: EC_PF_2:51
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 &amp; Q `3_3 <> 0 &amp; P `2_3 <> 0 &amp; P _EQ_ (compell_ProjCo (z,p)) . Q holds
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
proofend;

theorem ThECEQ4: :: EC_PF_2:52
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st not P _EQ_ Q &amp; P _EQ_ (compell_ProjCo (z,p)) . Q holds
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
proofend;

theorem ThNonSingular: :: EC_PF_2:53
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g3 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st g3 = 3 mod p &amp; P `2_3 = 0 &amp; P `3_3 <> 0 holds
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0
proofend;

theorem ThAddEllEq1: :: EC_PF_2:54
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) &amp; 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))] holds
(gf2 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
proofend;

theorem ThAddEllEq2: :: EC_PF_2:55
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) &amp; 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))] holds
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
proofend;

theorem ThAddEllEq3: :: EC_PF_2:56
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) &amp; 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))] holds
((((z `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_3))
proofend;

theorem ThAddEllEq4: :: EC_PF_2:57
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) &amp; 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))] holds
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
proofend;

theorem ThAddEllEq5: :: EC_PF_2:58
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) &amp; 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))] holds
(((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)
proofend;

theorem ThDobEllEq1: :: EC_PF_2:59
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) &amp; R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_3)))
proofend;

theorem ThDobEllEq2: :: EC_PF_2:60
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) &amp; R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g4 * (gf2 |^ 2)) * (P `3_3)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))
proofend;

theorem ThDobEllEq3: :: EC_PF_2:61
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) &amp; R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3))
proofend;

theorem ThDobEllEq4: :: EC_PF_2:62
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) &amp; R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))
proofend;

theorem ThDobEllEq5: :: EC_PF_2:63
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) &amp; R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((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)
proofend;

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
func addell_ProjCo (z,p) ->  Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) means :: EC_PF_2:def 9
 for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies it . (P,Q) = Q ) &amp; ( Q _EQ_ O &amp; not P _EQ_ O implies it . (P,Q) = P ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
it . (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))] ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) holds
it . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) );
existence
 ex b1 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) st
for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b1 . (P,Q) = Q ) &amp; ( Q _EQ_ O &amp; not P _EQ_ O implies b1 . (P,Q) = P ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b1 . (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))] ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b1 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) )
proofend;
uniqueness
 for b1, b2 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) st ( for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b1 . (P,Q) = Q ) &amp; ( Q _EQ_ O &amp; not P _EQ_ O implies b1 . (P,Q) = P ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b1 . (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))] ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b1 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) ) &amp; ( for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b2 . (P,Q) = Q ) &amp; ( Q _EQ_ O &amp; not P _EQ_ O implies b2 . (P,Q) = P ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b2 . (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))] ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b2 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines addell_ProjCo EC_PF_2:def_9_:_
 for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b3 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) holds
( b3 = addell_ProjCo (z,p) iff for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b3 . (P,Q) = Q ) &amp; ( Q _EQ_ O &amp; not P _EQ_ O implies b3 . (P,Q) = P ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p &amp; gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) &amp; gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) &amp; gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b3 . (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))] ) &amp; ( not P _EQ_ O &amp; not Q _EQ_ O &amp; P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p &amp; g3 = 3 mod p &amp; g4 = 4 mod p &amp; g8 = 8 mod p &amp; gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) &amp; gf2 = (P `2_3) * (P `3_3) &amp; gf3 = ((P `1_3) * (P `2_3)) * gf2 &amp; gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b3 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) );

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
let F be Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p));
let Q, R be Element of EC_SetProjCo ((z `1),(z `2),p);
:: original:.
redefine funcF . (Q,R) ->  Element of EC_SetProjCo ((z `1),(z `2),p);
correctness
coherence
F . (Q,R) is Element of EC_SetProjCo ((z `1),(z `2),p);
proofend;
end;