( 0. Z_3 = 0 & 1. Z_3 = 1 & 0. Z_3 is Element of {0,1,2} & 1. Z_3 is Element of {0,1,2} & the addF of Z_3 = add3 & the multF of Z_3 = mult3 ) ;