theorem Th24: :: IDEA_1:24

for i, j, n being Nat holds MUL_MOD (i,j,n) is_expressible_by n