let a, b be Integer; :: thesis: for 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) ) ) holds
{ i where i is Nat : B . i = 0 } is non empty Subset of NAT
let A, B be sequence of NAT; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Nat : B . i = 0 } is non empty Subset of NAT )
assume 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) ) ) ) ; :: thesis: { i where i is Nat : B . i = 0 } is non empty Subset of NAT
A2: for x being object st x in { i where i is Nat : B . i = 0 } holds
x in NAT

proof

let x be object ; :: thesis: ( x in { i where i is Nat : B . i = 0 } implies x in NAT )
assume x in { i where i is Nat : B . i = 0 } ; :: thesis: x in NAT
then ex i being Nat st
( x = i & B . i = 0 ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

ex m0 being Nat st B . m0 = 0

proof

assume A3: for m0 being Nat holds not B . m0 = 0 ; :: thesis: contradiction
A4: for i being Nat holds B . (i + 1) <= (B . i) - 1

proof

let i be Nat; :: thesis: B . (i + 1) <= (B . i) - 1
A5: B . i <> 0 by A3;
B . (i + 1) = (A . i) mod (B . i) by A1;
then (B . (i + 1)) + 1 <= B . i by NAT_1:13, A5, INT_1:58;
then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9;
hence B . (i + 1) <= (B . i) - 1 ; :: thesis: verum

end;

defpred S₁[ Nat] means B . $1 <= (B . 0) - $1;
A6: S₁[ 0 ] ;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A8: S₁[i] ; :: thesis: S₁[i + 1]
A9: B . (i + 1) <= (B . i) - 1 by A4;
(B . i) - 1 <= ((B . 0) - i) - 1 by A8, XREAL_1:9;
hence S₁[i + 1] by A9, XXREAL_0:2; :: thesis: verum

end;

A10: for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A7);
B . (B . 0) <= (B . 0) - (B . 0) by A10;
hence contradiction by A3, NAT_1:14; :: thesis: verum

end;

then consider m0 being Nat such that
A11: B . m0 = 0 ;
m0 in { i where i is Nat : B . i = 0 } by A11;
hence { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A2, TARSKI:def 3; :: thesis: verum