let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring F) st p gcd q <> 1_. F holds
deg (p gcd q) > 0
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of the carrier of (Polynom-Ring F) st p gcd q <> 1_. F holds
deg (p gcd q) > 0
let q be Element of the carrier of (Polynom-Ring F); :: thesis: ( p gcd q <> 1_. F implies deg (p gcd q) > 0 )
assume AS: p gcd q <> 1_. F ; :: thesis: deg (p gcd q) > 0
reconsider g = p gcd q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

now :: thesis: not g is constant

assume g is constant ; :: thesis: contradiction
then consider a being Element of F such that
A: g = a | F by RING_4:20;

now :: thesis: not a <> 1. F

assume a <> 1. F ; :: thesis: contradiction
then LC g <> 1. F by A, RING_5:6;
hence contradiction by RATFUNC1:def 7; :: thesis: verum

end;

hence contradiction by AS, A, RING_4:14; :: thesis: verum

end;

hence deg (p gcd q) > 0 by RING_4:def 4; :: thesis: verum