:: deftheorem defines MUL_MOD IDEA_1:def 9 :
for n, i, j being Nat holds MUL_MOD (i,j,n) = ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n);