let p be 5 _or_greater Prime; :: thesis:
let z be Element of EC_WParam p; :: thesis:
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis:
assume A3: ( P `3_3 = 1 & Q `3_3 = 1 ) ; :: thesis:
reconsider CP = (compell_ProjCo (z,p)) . P, CQ = (compell_ProjCo (z,p)) . Q as Element of EC_SetProjCo ((z `1),(z `2),p) ;
A4: ( CP = [(P `1_3),(- (P `2_3)),(P `3_3)] & CQ = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] ) by EC_PF_2:def 8;
then A5: ( CP `3_3 = 1 & CQ `3_3 = 1 ) by A3, EC_PF_2:def 5;
A6: ( CP `1_3 = P `1_3 & CP `2_3 = - (P `2_3) ) by A4, EC_PF_2:33;
A7: ( CQ `1_3 = Q `1_3 & CQ `2_3 = - (Q `2_3) ) by A4, EC_PF_2:33;
reconsider PQ = (addell_ProjCo (z,p)) . (P,Q) as Element of EC_SetProjCo ((z `1),(z `2),p) ;
reconsider CP = (compell_ProjCo (z,p)) . P, CQ = (compell_ProjCo (z,p)) . Q as Element of EC_SetProjCo ((z `1),(z `2),p) ;

reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
reconsider gf1 = (Q `2_3) - (P `2_3) as Element of (GF p) ;
reconsider gf2 = (Q `1_3) - (P `1_3) as Element of (GF p) ;
reconsider gf3 = ((gf1 |^ 2) - (gf2 |^ 3)) - ((g2 * (gf2 |^ 2)) * (P `1_3)) as Element of (GF p) ;
reconsider gf1C = (CQ `2_3) - (CP `2_3) as Element of (GF p) ;
reconsider gf2C = (CQ `1_3) - (CP `1_3) as Element of (GF p) ;
reconsider gf3C = ((gf1C |^ 2) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3)) as Element of (GF p) ;
B2: gf1C = (- (Q `2_3)) - (- (P `2_3)) by A4, A7, EC_PF_2:33
.= - ((- (P `2_3)) + (Q `2_3)) by RLVECT_1:31
.= - gf1 ;
B3: gf2C = (Q `1_3) - (CP `1_3) by A4, EC_PF_2:33
.= gf2 by A4, EC_PF_2:33 ;
B4: gf3C = ((gf1C * gf1C) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3)) by EC_PF_1:22
.= ((gf1 * gf1) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3)) by B2, EC_PF_1:26
.= ((gf1 |^ 2) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3)) by EC_PF_1:22
.= gf3 by A4, B3, EC_PF_2:33 ;
B5: PQ = [(gf2 * gf3),((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) - ((gf2 |^ 3) * (P `2_3))),(gf2 |^ 3)] by A3, B1, LmAddEll1;
(addell_ProjCo (z,p)) . (CP,CQ) = [(gf2C * gf3C),((gf1C * (((gf2C |^ 2) * (CP `1_3)) - gf3C)) - ((gf2C |^ 3) * (CP `2_3))),(gf2C |^ 3)] by A5, B1, LmAddEll1, EC_PF_2:46
.= [(gf2 * gf3),(((- gf1) * (((gf2 |^ 2) * (P `1_3)) - gf3)) - (- ((gf2 |^ 3) * (P `2_3)))),(gf2 |^ 3)] by A6, B2, B3, B4, VECTSP_1:8
.= [(gf2 * gf3),((- (gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3))) - (- ((gf2 |^ 3) * (P `2_3)))),(gf2 |^ 3)] by VECTSP_1:8
.= [(gf2 * gf3),(- ((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) + (- ((gf2 |^ 3) * (P `2_3))))),(gf2 |^ 3)] by RLVECT_1:31
.= [(PQ `1_3),(- ((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) - ((gf2 |^ 3) * (P `2_3)))),(gf2 |^ 3)] by B5, EC_PF_2:33
.= [(PQ `1_3),(- (PQ `2_3)),(gf2 |^ 3)] by B5, EC_PF_2:33
.= [(PQ `1_3),(- (PQ `2_3)),(PQ `3_3)] by B5, EC_PF_2:33 ;
hence (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q)) by EC_PF_2:def 8; :: thesis:

end;

suppose B1: P _EQ_ Q ; :: thesis:

reconsider g2 = 2 mod p, g3 = 3 mod p, g4 = 4 mod p, g8 = 8 mod p as Element of (GF p) by EC_PF_1:14;
reconsider gf1 = (z `1) + (g3 * ((P `1_3) |^ 2)), gf2 = P `2_3 as Element of (GF p) ;
reconsider gf3 = ((P `1_3) * (P `2_3)) * gf2 as Element of (GF p) ;
reconsider gf4 = (gf1 |^ 2) - (g8 * gf3) as Element of (GF p) ;
reconsider gf1C = (z `1) + (g3 * ((CP `1_3) |^ 2)), gf2C = CP `2_3 as Element of (GF p) ;
reconsider gf3C = ((CP `1_3) * (CP `2_3)) * gf2C as Element of (GF p) ;
reconsider gf4C = (gf1C |^ 2) - (g8 * gf3C) as Element of (GF p) ;
B2: gf1C = gf1 by A4, EC_PF_2:33;
B3: gf2C = - gf2 by A4, EC_PF_2:33;
B4: gf3C = (P `1_3) * ((- (P `2_3)) * (- gf2)) by A6, GROUP_1:def 3
.= (P `1_3) * ((P `2_3) * gf2) by VECTSP_1:10
.= gf3 by GROUP_1:def 3 ;
B6: gf2C |^ 2 = gf2C * gf2C by EC_PF_1:22
.= gf2 * gf2 by B3, EC_PF_1:26
.= gf2 |^ 2 by EC_PF_1:22 ;
B7: (CP `2_3) |^ 2 = (CP `2_3) * (CP `2_3) by EC_PF_1:22
.= (P `2_3) * (P `2_3) by A6, EC_PF_1:26
.= (P `2_3) |^ 2 by EC_PF_1:22 ;
B8: gf2C |^ 3 = gf2C |^ (2 + 1)
.= (gf2C |^ 2) * gf2C by EC_PF_1:24
.= - ((gf2 |^ 2) * gf2) by B3, B6, VECTSP_1:8
.= - (gf2 |^ (2 + 1)) by EC_PF_1:24
.= - (gf2 |^ 3) ;
B9: PQ = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] by A3, B1, LmAddEll2;
B11: (addell_ProjCo (z,p)) . (CP,CQ) = [((g2 * gf4C) * gf2C),((gf1C * ((g4 * gf3C) - gf4C)) - ((g8 * ((CP `2_3) |^ 2)) * (gf2C |^ 2))),(g8 * (gf2C |^ 3))] by A5, B1, LmAddEll2, EC_PF_2:46
.= [(- ((g2 * gf4) * gf2)),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (- (gf2 |^ 3)))] by B2, B3, B4, B7, B8, VECTSP_1:8
.= [(- ((g2 * gf4) * gf2)),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(- (g8 * (gf2 |^ 3)))] by VECTSP_1:8
.= [(- (PQ `1_3)),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(- (g8 * (gf2 |^ 3)))] by B9, EC_PF_2:33
.= [(- (PQ `1_3)),(PQ `2_3),(- (g8 * (gf2 |^ 3)))] by B9, EC_PF_2:33
.= [(- (PQ `1_3)),(PQ `2_3),(- (PQ `3_3))] by B9, EC_PF_2:33 ;
B12: (compell_ProjCo (z,p)) . PQ = [(PQ `1_3),(- (PQ `2_3)),(PQ `3_3)] by EC_PF_2:def 8;
B13: ((addell_ProjCo (z,p)) . (CP,CQ)) `1_3 = - ((1. (GF p)) * (PQ `1_3)) by B11, EC_PF_2:33
.= (- (1. (GF p))) * (PQ `1_3) by VECTSP_1:9
.= (- (1. (GF p))) * (((compell_ProjCo (z,p)) . PQ) `1_3) by B12, EC_PF_2:33 ;
B14: ((addell_ProjCo (z,p)) . (CP,CQ)) `2_3 = (1. (GF p)) * (PQ `2_3) by B11, EC_PF_2:33
.= (- (1. (GF p))) * (- (PQ `2_3)) by VECTSP_1:10
.= (- (1. (GF p))) * (((compell_ProjCo (z,p)) . PQ) `2_3) by B12, EC_PF_2:33 ;
B15: ((addell_ProjCo (z,p)) . (CP,CQ)) `3_3 = - ((1. (GF p)) * (PQ `3_3)) by B11, EC_PF_2:33
.= (- (1. (GF p))) * (PQ `3_3) by VECTSP_1:9
.= (- (1. (GF p))) * (((compell_ProjCo (z,p)) . PQ) `3_3) by B12, EC_PF_2:33 ;
- (1. (GF p)) <> 0. (GF p)

proof

assume - (1. (GF p)) = 0. (GF p) ; :: thesis:
then (1. (GF p)) - (1. (GF p)) = 1. (GF p) by RLVECT_1:4;
then 0. (GF p) = 1. (GF p) by RLVECT_1:15;
hence contradiction ; :: thesis:

end;

hence (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q)) by B13, B14, B15, ThEQX; :: thesis:

end;