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_{1} 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_{1} = A . (min* { i where i is Nat : B . i = 0 } ) )
by A1; :: thesis: verum

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

( 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