let F be Field; :: thesis: for p being Polynomial of F
for q being non zero Polynomial of F
for s being monic Polynomial of F holds
( s = p gcd q iff ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) )
let p be Polynomial of F; :: thesis: for q being non zero Polynomial of F
for s being monic Polynomial of F holds
( s = p gcd q iff ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) )
let q be non zero Polynomial of F; :: thesis: for s being monic Polynomial of F holds
( s = p gcd q iff ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) )
let s be monic Polynomial of F; :: thesis: ( s = p gcd q iff ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) )

now :: thesis: ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) implies s = p gcd q )

assume AS: ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) ; :: thesis: s = p gcd q
reconsider a = p, b = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider g = s as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
B: b <> 0_. F ;

now :: thesis: for d being Element of (Polynom-Ring F) st d divides a & d divides b holds
d divides g

let d be Element of (Polynom-Ring F); :: thesis: ( d divides a & d divides b implies d divides g )
assume C: ( d divides a & d divides b ) ; :: thesis: d divides g
reconsider h = d as Polynomial of F by POLYNOM3:def 10;
( h divides p & h divides q ) by C;
then h divides s by AS;
hence d divides g ; :: thesis: verum

end;

then g is a,b -gcd by AS;
then g = a gcd b by dpg, B;
hence s = p gcd q by dd; :: thesis: verum

end;

hence ( s = p gcd q iff ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) ) by G1; :: thesis: verum