let x, p, y be Element of INT ; :: thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p )
assume A1: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 ) ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

per cases ( p = 0 or p <> 0 ) ;

suppose A2: p = 0 ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

hence ((ALGO_INVERSE (x,p)) * x) mod p = 0 by INT_1:def 10
.= 1 mod p by A2, INT_1:def 10 ;
:: thesis: verum

end;

suppose p <> 0 ; :: thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p

hence ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p by Lm13, A1; :: thesis: verum

end;

end;