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));

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)) <> {}

hence
the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) = {}
; :: thesis: verumassume 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;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