theorem Th22: :: IDEA_1:22

for i, n being Nat st i is_expressible_by n holds
MUL_MOD (1,i,n) = i