p <> 1 by INT_2:def 4;
hence for b₁ being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p implies ( b₁ = LegendreSymbol (a,p) iff b₁ = 1 ) ) & ( p divides a implies ( b₁ = LegendreSymbol (a,p) iff b₁ = 0 ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b₁ = LegendreSymbol (a,p) iff b₁ = - 1 ) ) ) by Def3; :: thesis: verum