let n be Nat; :: thesis: ( 1 < n implies 0. (Z/ n) = 0 )
Z/ n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) by INT_3:def 12;
hence ( 1 < n implies 0. (Z/ n) = 0 ) by NAT_1:44, SUBSET_1:def 8; :: thesis: verum