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

now :: thesis: F_Real is polynomial_disjoint

assume not F_Real is polynomial_disjoint ; :: thesis: contradiction
then ( the Element of ([#] F_Real) /\ ([#] (Polynom-Ring F_Real)) in [#] F_Real & the Element of ([#] F_Real) /\ ([#] (Polynom-Ring F_Real)) in [#] (Polynom-Ring F_Real) ) by XBOOLE_0:def 4;
then reconsider p = the Element of ([#] F_Real) /\ ([#] (Polynom-Ring F_Real)) as Polynomial of F_Real by POLYNOM3:def 10;
reconsider x = the Element of ([#] F_Real) /\ ([#] (Polynom-Ring F_Real)) as Real ;
p = x ;
hence contradiction by Th21; :: thesis: verum

end;

hence F_Real is polynomial_disjoint ; :: thesis: verum