set R = F_Rat ;

set x = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat));

set x = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat));

now :: thesis: F_Rat is polynomial_disjoint

hence
F_Rat is polynomial_disjoint
; :: thesis: verumassume
not F_Rat is polynomial_disjoint
; :: thesis: contradiction

then A1: ( the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) in [#] F_Rat & the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) in [#] (Polynom-Ring F_Rat) ) by XBOOLE_0:def 4;

then reconsider p = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) as Polynomial of F_Rat by POLYNOM3:def 10;

reconsider x = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) as Rational by A1;

p = x ;

hence contradiction by Th20; :: thesis: verum

end;then A1: ( the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) in [#] F_Rat & the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) in [#] (Polynom-Ring F_Rat) ) by XBOOLE_0:def 4;

then reconsider p = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) as Polynomial of F_Rat by POLYNOM3:def 10;

reconsider x = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) as Rational by A1;

p = x ;

hence contradiction by Th20; :: thesis: verum