theorem Th15: :: IDEA_1:15

for i, j, n being Nat holds ADD_MOD (i,j,n) is_expressible_by n by NAT_D:1, POWER:34;