Z/ n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #)
by INT_3:def 12;

then A1: [#] (Z/ n) = n by ORDINAL1:def 17;

set M = ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n)));

set x = the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n)));

then A1: [#] (Z/ n) = n by ORDINAL1:def 17;

set M = ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n)));

set x = the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n)));

now :: thesis: Z/ n is polynomial_disjoint

hence
Z/ n is polynomial_disjoint
; :: thesis: verumassume
not Z/ n is polynomial_disjoint
; :: thesis: contradiction

then A2: ( the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) in [#] (Z/ n) & the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) in [#] (Polynom-Ring (Z/ n)) ) by XBOOLE_0:def 4;

then reconsider p = the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) as Polynomial of (Z/ n) by POLYNOM3:def 10;

the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) in { m where m is Nat : m < n } by A1, A2, Th1;

then consider m being Nat such that

A3: ( the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) = m & m < n ) ;

m = p by A3;

hence contradiction by Th18; :: thesis: verum

end;then A2: ( the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) in [#] (Z/ n) & the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) in [#] (Polynom-Ring (Z/ n)) ) by XBOOLE_0:def 4;

then reconsider p = the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) as Polynomial of (Z/ n) by POLYNOM3:def 10;

the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) in { m where m is Nat : m < n } by A1, A2, Th1;

then consider m being Nat such that

A3: ( the Element of ([#] (Z/ n)) /\ ([#] (Polynom-Ring (Z/ n))) = m & m < n ) ;

m = p by A3;

hence contradiction by Th18; :: thesis: verum