:: deftheorem Def20 defines Z_3 MOD_2:def 20 :
Z_3 = doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #);