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