let n be non trivial Nat; :: thesis: for p being Element of the carrier of (Polynom-Ring (Z/ n)) holds the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) = {}
let p be Element of the carrier of (Polynom-Ring (Z/ n)); :: thesis: the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) = {}
set F = Z/ n;
set FX = Polynom-Ring (Z/ n);
set I = {p} -Ideal ;
set K = (Polynom-Ring (Z/ n)) / ({p} -Ideal);
set x = the Element of the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal));

now :: thesis: not the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) <> {}

assume AS: the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) <> {} ; :: thesis: contradiction
reconsider x = the Element of the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) as Element of (Z/ n) by AS, XBOOLE_0:def 4;
reconsider q = x as Element of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) by AS, XBOOLE_0:def 4;
consider a being Element of (Polynom-Ring (Z/ n)) such that
A1: q = Class ((EqRel ((Polynom-Ring (Z/ n)),({p} -Ideal))),a) by RING_1:11;
reconsider pa = a as Polynomial of (Z/ n) by POLYNOM3:def 10;
a - a = 0. (Polynom-Ring (Z/ n)) by RLVECT_1:15;
then A2: a in q by A1, RING_1:5, IDEAL_1:3;
Z/ n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) by INT_3:def 12;
then x in Segm n ;
then reconsider k = x as Element of omega ;
k = { m where m is Nat : m < k } by AXIOMS:4;
then consider m being Nat such that
B1: ( a = m & m < k ) by A2;
dom pa = NAT by FUNCT_2:def 1;
hence contradiction by B1; :: thesis: verum

end;

hence the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) = {} ; :: thesis: verum