Z/ n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) by INT_3:def 12;
hence Z/ n is strong_polynomial_disjoint by FIELD_3:24; :: thesis: verum