per cases ( ( p = 0_. F & q = 0_. F ) or p <> 0_. F or q <> 0_. F ) ;

suppose ( p = 0_. F & q = 0_. F ) ; :: thesis: for b₁, b₂ being Element of the carrier of (Polynom-Ring F) holds
( ( p = 0_. F & q = 0_. F & b₁ = 0_. F & b₂ = 0_. F implies b₁ = b₂ ) & ( ( not p = 0_. F or not q = 0_. F ) & b₁ is a_gcd of p,q & b₁ is monic & b₂ is a_gcd of p,q & b₂ is monic implies b₁ = b₂ ) )

hence for b₁, b₂ being Element of the carrier of (Polynom-Ring F) holds
( ( p = 0_. F & q = 0_. F & b₁ = 0_. F & b₂ = 0_. F implies b₁ = b₂ ) & ( ( not p = 0_. F or not q = 0_. F ) & b₁ is a_gcd of p,q & b₁ is monic & b₂ is a_gcd of p,q & b₂ is monic implies b₁ = b₂ ) ) ; :: thesis: verum

end;

suppose ( p <> 0_. F or q <> 0_. F ) ; :: thesis: for b₁, b₂ being Element of the carrier of (Polynom-Ring F) holds
( ( p = 0_. F & q = 0_. F & b₁ = 0_. F & b₂ = 0_. F implies b₁ = b₂ ) & ( ( not p = 0_. F or not q = 0_. F ) & b₁ is a_gcd of p,q & b₁ is monic & b₂ is a_gcd of p,q & b₂ is monic implies b₁ = b₂ ) )

thus for b₁, b₂ being Element of the carrier of (Polynom-Ring F) holds
( ( p = 0_. F & q = 0_. F & b₁ = 0_. F & b₂ = 0_. F implies b₁ = b₂ ) & ( ( not p = 0_. F or not q = 0_. F ) & b₁ is a_gcd of p,q & b₁ is monic & b₂ is a_gcd of p,q & b₂ is monic implies b₁ = b₂ ) ) by gcd1, np0; :: thesis: verum

end;

end;