theorem :: IDEA_1:21

for i, j, n being Nat holds MUL_MOD (i,j,n) = MUL_MOD (j,i,n) ;