reconsider y = x mod p as Element of INT by INT_1:def 2;

now :: thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

per cases ( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 ) ;

suppose A1: (ALGO_EXGCD (p,y)) `3_3 = 1 ; :: thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

now :: thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

per cases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ;

suppose A2: (ALGO_EXGCD (p,y)) `2_3 < 0 ; :: thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

reconsider z = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ;
reconsider s = p + z as Element of INT by INT_1:def 2;
ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ;
hence ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A2, A1; :: thesis: verum

end;

suppose A3: 0 <= (ALGO_EXGCD (p,y)) `2_3 ; :: thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

reconsider s = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ;
thus ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A3, A1; :: thesis: verum

end;

end;

end;

hence ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ; :: thesis: verum

end;

suppose A4: (ALGO_EXGCD (p,y)) `3_3 <> 1 ; :: thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )

reconsider s = {} as Element of INT by INT_1:def 2;
( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ;
hence ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A4; :: thesis: verum

end;

end;

end;

then consider s being Element of INT such that
A5: ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ;
take s ; :: thesis: for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) )
thus for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by A5; :: thesis: verum