let a, b be Integer; :: thesis: ALGO_GCD (a,b) = a gcd b
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) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Nat : B . i = 0 } ) ) by Def1;
set m0 = min* { i where i is Nat : B . i = 0 } ;
A2: { i where i is Nat : B . i = 0 } is non empty Subset of NAT by A1, Lm5;
then min* { i where i is Nat : B . i = 0 } in { i where i is Nat : B . i = 0 } by NAT_1:def 1;
then A3: ex i being Nat st
( min* { i where i is Nat : B . i = 0 } = i & B . i = 0 ) ;

per cases ( min* { i where i is Nat : B . i = 0 } = 0 or min* { i where i is Nat : B . i = 0 } <> 0 ) ;

suppose min* { i where i is Nat : B . i = 0 } = 0 ; :: thesis: ALGO_GCD (a,b) = a gcd b

hence ALGO_GCD (a,b) = (A . 0) gcd (B . 0) by A3, NEWTON:52, A1
.= a gcd b by A1, INT_2:34 ;
:: thesis: verum

end;

suppose min* { i where i is Nat : B . i = 0 } <> 0 ; :: thesis: ALGO_GCD (a,b) = a gcd b

then 1 - 1 <= (min* { i where i is Nat : B . i = 0 } ) - 1 by XREAL_1:9, NAT_1:14;
then reconsider m1 = (min* { i where i is Nat : B . i = 0 } ) - 1 as Element of NAT by INT_1:3;
A5: B . m1 <> 0

proof

assume B . m1 = 0 ; :: thesis: contradiction
then A6: m1 in { i where i is Nat : B . i = 0 } ;
(min* { i where i is Nat : B . i = 0 } ) - 1 < (min* { i where i is Nat : B . i = 0 } ) - 0 by XREAL_1:15;
hence contradiction by A6, A2, NAT_1:def 1; :: thesis: verum

end;

then A7: (A . 0) gcd (B . 0) = (A . m1) gcd (B . m1) by A1, Lm4;
A8: (A . m1) gcd (B . m1) = (A . (m1 + 1)) gcd (B . (m1 + 1)) by Lm3, A5, A1;
(A . (min* { i where i is Nat : B . i = 0 } )) gcd (B . (min* { i where i is Nat : B . i = 0 } )) = ALGO_GCD (a,b) by A1, NEWTON:52, A3;
hence ALGO_GCD (a,b) = a gcd b by A8, A7, A1, INT_2:34; :: thesis: verum

end;

end;