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)));
now :: thesis: Z/ n is polynomial_disjoint
assume 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;
hence Z/ n is polynomial_disjoint ; :: thesis: verum