consider g, w, q, t, a, b, v, u being sequence of INT such that
A1: ( 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 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 Lm6;
set istop = min* { i where i is Nat : w . i = 0 } ;
now :: thesis: ex xx being Element of st
( ( 0 <= g . (min* { i where i is Nat : w . i = 0 } ) implies xx = [(a . (min* { i where i is Nat : w . i = 0 } )),(b . (min* { i where i is Nat : w . i = 0 } )),(g . (min* { i where i is Nat : w . i = 0 } ))] ) & ( g . (min* { i where i is Nat : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Nat : w . i = 0 } ))),(- (b . (min* { i where i is Nat : w . i = 0 } ))),(- (g . (min* { i where i is Nat : w . i = 0 } )))] ) )
per cases ( 0 <= g . (min* { i where i is Nat : w . i = 0 } ) or g . (min* { i where i is Nat : w . i = 0 } ) < 0 ) ;
suppose A2: 0 <= g . (min* { i where i is Nat : w . i = 0 } ) ; :: thesis: ex xx being Element of st
( ( 0 <= g . (min* { i where i is Nat : w . i = 0 } ) implies xx = [(a . (min* { i where i is Nat : w . i = 0 } )),(b . (min* { i where i is Nat : w . i = 0 } )),(g . (min* { i where i is Nat : w . i = 0 } ))] ) & ( g . (min* { i where i is Nat : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Nat : w . i = 0 } ))),(- (b . (min* { i where i is Nat : w . i = 0 } ))),(- (g . (min* { i where i is Nat : w . i = 0 } )))] ) )

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

A4: - (g . (min* { i where i is Nat : w . i = 0 } )) in INT by INT_1:def 2;
( - (a . (min* { i where i is Nat : w . i = 0 } )) in INT & - (b . (min* { i where i is Nat : w . i = 0 } )) in INT ) by INT_1:def 2;
then [(- (a . (min* { i where i is Nat : w . i = 0 } ))),(- (b . (min* { i where i is Nat : w . i = 0 } ))),(- (g . (min* { i where i is Nat : w . i = 0 } )))] in by ;
hence ex xx being Element of st
( ( 0 <= g . (min* { i where i is Nat : w . i = 0 } ) implies xx = [(a . (min* { i where i is Nat : w . i = 0 } )),(b . (min* { i where i is Nat : w . i = 0 } )),(g . (min* { i where i is Nat : w . i = 0 } ))] ) & ( g . (min* { i where i is Nat : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Nat : w . i = 0 } ))),(- (b . (min* { i where i is Nat : w . i = 0 } ))),(- (g . (min* { i where i is Nat : w . i = 0 } )))] ) ) by A3; :: thesis: verum
end;
end;
end;
then consider xx being Element of such that
A5: ( ( 0 <= g . (min* { i where i is Nat : w . i = 0 } ) implies xx = [(a . (min* { i where i is Nat : w . i = 0 } )),(b . (min* { i where i is Nat : w . i = 0 } )),(g . (min* { i where i is Nat : w . i = 0 } ))] ) & ( g . (min* { i where i is Nat : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Nat : w . i = 0 } ))),(- (b . (min* { i where i is Nat : w . i = 0 } ))),(- (g . (min* { i where i is Nat : w . i = 0 } )))] ) ) ;
take xx ; :: thesis: ex g, w, q, t, a, b, v, u being sequence of INT ex istop being 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 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 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 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 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 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 A1, A5; :: thesis: verum