consider A, B being sequence of NAT such that
A1: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being 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 Nat : B . i = 0 } );
A . (min* { i where i is 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 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₁ = A . (min* { i where i is Nat : B . i = 0 } ) ) by A1; :: thesis: verum