let a, b be Element of INT ; :: thesis: for A, B being sequence of INT 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 INT; :: 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:
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 m0 being Nat holds |.(B . m0).| <> 0 by ;
A5: for i being Nat holds |.(B . (i + 1)).| <= |.(B . i).| - 1
proof
let i be Nat; :: thesis: |.(B . (i + 1)).| <= |.(B . i).| - 1
|.(B . (i + 1)).| = |.((A . i) mod (B . i)).| by A1;
then |.(B . (i + 1)).| < |.(B . i).| by ;
then |.(B . (i + 1)).| + 1 <= |.(B . i).| by NAT_1:13;
then (|.(B . (i + 1)).| + 1) - 1 <= |.(B . i).| - 1 by XREAL_1:9;
hence |.(B . (i + 1)).| <= |.(B . i).| - 1 ; :: thesis: verum
end;
defpred S1[ Nat] means |.(B . \$1).| <= |.(B . 0).| - \$1;
A6: S1[ 0 ] ;
A7: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A8: S1[i] ; :: thesis: S1[i + 1]
A9: |.(B . (i + 1)).| <= |.(B . i).| - 1 by A5;
|.(B . i).| - 1 <= (|.(B . 0).| - i) - 1 by ;
hence S1[i + 1] by ; :: thesis: verum
end;
A10: for i being Nat holds S1[i] from NAT_1:sch 2(A6, A7);
|.(B . |.(B . 0).|).| <= |.(B . 0).| - |.(B . 0).| by A10;
hence contradiction by A4, 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 ; :: thesis: verum