consider g, w, q, t, a, b, v, u being sequence of INT such that
P1: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) by EXLM1;
set istop = min* { i where i is Element of NAT : w . i = 0 } ;

now :: thesis: ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) )

per cases ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) or g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 ) ;

suppose C1: 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) ; :: thesis: ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) )

[(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] in [:INT,INT,INT:] by MCART_1:69;
hence ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) by C1; :: thesis: verum

end;

suppose C2: g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 ; :: thesis: ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) )

X1: - (g . (min* { i where i is Element of NAT : w . i = 0 } )) in INT by INT_1:def 2;
( - (a . (min* { i where i is Element of NAT : w . i = 0 } )) in INT & - (b . (min* { i where i is Element of NAT : w . i = 0 } )) in INT ) by INT_1:def 2;
then [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] in [:INT,INT,INT:] by MCART_1:69, X1;
hence ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) by C2; :: thesis: verum

end;

end;

end;

then consider xx being Element of [:INT,INT,INT:] such that
P2: ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) ;
take xx ; :: thesis: ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies xx = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies xx = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) )
thus ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies xx = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies xx = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) by P1, P2; :: thesis: verum