for i, j, k, n being Nat st (2 to_power n) + 1 is prime & i is_expressible_by n & j is_expressible_by n & k is_expressible_by n holds
MUL_MOD ((MUL_MOD (i,j,n)),k,n) = MUL_MOD (i,(MUL_MOD (j,k,n)),n)