set a = 1. (GF p);
set b = 0. (GF p);
reconsider g2 = 2 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 g27 = 27 mod p as Element of (GF p) by EC_PF_1:14;
A1: g4 = (2 * 2) mod p
.= g2 * g2 by EC_PF_1:18
.= g2 |^ 2 by EC_PF_1:22 ;
p >= 4 + 1 by Def1;
then A2: ( p > 2 & p > 3 ) by XXREAL_0:2;
Disc ((1. (GF p)),(0. (GF p)),p) = (g4 * ((1. (GF p)) |^ (2 + 1))) + (g27 * ((0. (GF p)) |^ 2)) by EC_PF_1:def 7
.= (g4 * (((1. (GF p)) |^ 2) * (1. (GF p)))) + (g27 * ((0. (GF p)) |^ 2)) by EC_PF_1:24
.= (g4 * (((1. (GF p)) |^ 2) * (1. (GF p)))) + (g27 * ((0. (GF p)) * (0. (GF p)))) by EC_PF_1:22
.= (g4 * (((1. (GF p)) * (1. (GF p))) * (1. (GF p)))) + (g27 * ((0. (GF p)) * (0. (GF p)))) by EC_PF_1:22
.= g4 * (1. (GF p)) by ALGSTR_1:7
.= g4 ;
then A3: Disc ((1. (GF p)),(0. (GF p)),p) <> 0. (GF p) by A1, A2, Th28;
take 1. (GF p) ; :: thesis: ex b being Element of (GF p) st [(1. (GF p)),b] in EC_WParam p
take 0. (GF p) ; :: thesis: [(1. (GF p)),(0. (GF p))] in EC_WParam p
thus [(1. (GF p)),(0. (GF p))] in EC_WParam p by A3; :: thesis: verum