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

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