let F be Field; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F) holds
( p gcd q divides p & p gcd q divides q & ( for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides p gcd q ) )
let p, q be Element of the carrier of (Polynom-Ring F); :: thesis: ( p gcd q divides p & p gcd q divides q & ( for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides p gcd q ) )
set g = p gcd q;
reconsider g1 = p gcd q as Element of (Polynom-Ring F) ;
( g1 divides p & g1 divides q ) by defGCD;
hence ( p gcd q divides p & p gcd q divides q ) ; :: thesis: for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides p gcd q
now :: thesis: for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides p gcd q
let r be Element of the carrier of (Polynom-Ring F); :: thesis: ( r divides p & r divides q implies r divides p gcd q )
reconsider r1 = r as Element of (Polynom-Ring F) ;
assume ( r divides p & r divides q ) ; :: thesis: r divides p gcd q
then r1 divides g1 by defGCD;
hence r divides p gcd q ; :: thesis: verum
end;
hence for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides p gcd q ; :: thesis: verum