let p be non constant Element of the carrier of (Polynom-Ring F_Rat); :: thesis: F_Rat ,(Polynom-Ring F_Rat) / ({p} -Ideal) are_disjoint
set F = F_Rat ;
set KR = (Polynom-Ring F_Rat) / ({p} -Ideal);
X: ( [#] F_Rat = the carrier of F_Rat & [#] ((Polynom-Ring F_Rat) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) ) ;
the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {} by Disj2;
hence F_Rat ,(Polynom-Ring F_Rat) / ({p} -Ideal) are_disjoint by X, FIELD_2:def 1; :: thesis: verum