consider A, B being sequence of NAT such that
P1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by LM1;
set m = A . (min* { i where i is Element of NAT : B . i = 0 } );
A . (min* { i where i is Element of NAT : B . i = 0 } ) is Element of NAT ;
hence ex b₁ being Element of NAT ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₁ = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) by P1; :: thesis: verum