let p be Prime; :: thesis: for a being Element of (GF p) st 2 < p holds
card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
let a be Element of (GF p); :: thesis: ( 2 < p implies card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) )
assume A1: 2 < p ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

per cases ( a is quadratic_residue or not a is quadratic_residue ) ;

suppose A2: a is quadratic_residue ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

then consider x being Element of (GF p) such that
A3: x |^ 2 = a ;
A4: x in { b where b is Element of (GF p) : b |^ 2 = a } by A3;
(- x) |^ 2 = (- x) * (- x) by Lm2
.= x * x by VECTSP_1:10
.= a by A3, Lm2 ;
then - x in { b where b is Element of (GF p) : b |^ 2 = a } ;
then A5: {x,(- x)} c= { b where b is Element of (GF p) : b |^ 2 = a } by A4, ZFMISC_1:32;
A6: x <> - x

proof

assume x = - x ; :: thesis: contradiction
then x + x = 0. (GF p) by VECTSP_1:16;
then A7: x = 0. (GF p) by A1, Th27;
x |^ 2 = (0. (GF p)) * (0. (GF p)) by A7, Lm2
.= 0. (GF p)
.= 0 by Th11 ;
hence contradiction by A3, A2; :: thesis: verum

end;

now :: thesis: for y being object st y in { b where b is Element of (GF p) : b |^ 2 = a } holds
y in {x,(- x)}

let y be object ; :: thesis: ( y in { b where b is Element of (GF p) : b |^ 2 = a } implies y in {x,(- x)} )
assume y in { b where b is Element of (GF p) : b |^ 2 = a } ; :: thesis: y in {x,(- x)}
then consider z being Element of (GF p) such that
A8: ( y = z & z |^ 2 = a ) ;
z * z = z |^ 2 by Lm2
.= x * x by A3, A8, Lm2 ;
then ( z = x or z = - x ) by Th26;
hence y in {x,(- x)} by A8, TARSKI:def 2; :: thesis: verum

end;

then { b where b is Element of (GF p) : b |^ 2 = a } c= {x,(- x)} ;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = card {x,(- x)} by A5, XBOOLE_0:def 10
.= 1 + 1 by A6, CARD_2:57
.= 1 + (Lege_p a) by A2, Def5 ;
:: thesis: verum

end;

suppose A9: not a is quadratic_residue ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

now :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

per cases ( a = 0 or a <> 0 ) ;

suppose A10: a = 0 ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) :: thesis: verum

proof

now :: thesis: for x being object st x in { b where b is Element of (GF p) : b |^ 2 = a } holds
x in {(0. (GF p))}

let x be object ; :: thesis: ( x in { b where b is Element of (GF p) : b |^ 2 = a } implies x in {(0. (GF p))} )
assume x in { b where b is Element of (GF p) : b |^ 2 = a } ; :: thesis: x in {(0. (GF p))}
then consider b being Element of (GF p) such that
A11: ( x = b & b |^ 2 = 0 ) by A10;
b = 0 by Th25, A11
.= 0. (GF p) by Th11 ;
hence x in {(0. (GF p))} by A11, TARSKI:def 1; :: thesis: verum

end;

then A12: { b where b is Element of (GF p) : b |^ 2 = a } c= {(0. (GF p))} ;
(0. (GF p)) |^ 2 = (0. (GF p)) * (0. (GF p)) by Lm2
.= 0. (GF p)
.= 0 by Th11 ;
then 0. (GF p) in { b where b is Element of (GF p) : b |^ 2 = a } by A10;
then {(0. (GF p))} c= { b where b is Element of (GF p) : b |^ 2 = a } by ZFMISC_1:31;
then { b where b is Element of (GF p) : b |^ 2 = a } = {(0. (GF p))} by A12, XBOOLE_0:def 10;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + 0 by CARD_2:42
.= 1 + (Lege_p a) by A10, Def5 ;
:: thesis: verum

end;

end;

suppose A13: a <> 0 ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

A14: { b where b is Element of (GF p) : b |^ 2 = a } = {}

proof

assume { b where b is Element of (GF p) : b |^ 2 = a } <> {} ; :: thesis: contradiction
then consider x being object such that
A15: x in { b where b is Element of (GF p) : b |^ 2 = a } by XBOOLE_0:def 1;
ex b being Element of (GF p) st
( x = b & b |^ 2 = a ) by A15;
hence contradiction by A9, A13; :: thesis: verum

end;

thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (- 1) by A14
.= 1 + (Lege_p a) by A9, A13, Def5 ; :: thesis: verum

end;

end;

end;

hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ; :: thesis: verum

end;

end;