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

suppose A: ( p = 0_. F & q = 0_. F ) ; :: thesis: p gcd q is p,q -gcd

reconsider g = p gcd q as Element of (Polynom-Ring F) ;
( g divides p & g divides q ) by A, dpg;
hence p gcd q is p,q -gcd by A, dpg; :: thesis: verum

end;

suppose A: ( p <> 0_. F or q <> 0_. F ) ; :: thesis: p gcd q is p,q -gcd

set g = p gcd q;
reconsider p1 = p, q1 = q as Element of (Polynom-Ring F) ;
set g1 = p1 gcd q1;
reconsider g1 = p1 gcd q1 as Element of (Polynom-Ring F) ;
thus p gcd q is p,q -gcd by A, dpg; :: thesis: verum

end;

end;