theorem Th7: :: NTALGO_1:7

for x, p, y being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 holds
((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p