:: deftheorem defines dL-Z_2 REALSET2:def 3 :
dL-Z_2 = doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);