let p be Prime; :: thesis: Lege (1,p) = 1
Lege ((1 ^2),p) = 1 by Th26;
hence Lege (1,p) = 1 ; :: thesis: verum