let a be Integer; :: thesis: for p being Prime holds Lege (a,p) = Leg (a,p)
let p be Prime; :: thesis: Lege (a,p) = Leg (a,p)

per cases ( Leg (a,p) = 1 or Leg (a,p) = 0 or Leg (a,p) = - 1 ) by Th24;

suppose A1: Leg (a,p) = 1 ; :: thesis: Lege (a,p) = Leg (a,p)

then not p divides a by Th25;
then a mod p <> 0 by INT_1:62;
hence Lege (a,p) = Leg (a,p) by A1, INT_5:def 3, Th25; :: thesis: verum

end;

suppose A2: Leg (a,p) = 0 ; :: thesis: Lege (a,p) = Leg (a,p)

then A3: p divides a by Th25;
p divides - a by A2, Th25, INT_2:10;
then A4: ((0 ^2) - a) mod p = 0 by INT_1:62;
a mod p = 0 by A3, INT_1:62;
hence Lege (a,p) = Leg (a,p) by A2, A4, INT_5:def 3, INT_5:def 2; :: thesis: verum

end;

suppose Leg (a,p) = - 1 ; :: thesis: Lege (a,p) = Leg (a,p)

hence Lege (a,p) = Leg (a,p) by Th25, INT_5:def 3; :: thesis: verum

end;

end;