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

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