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
for i being Nat st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
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 for i being Nat st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i) )
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: for i being Nat st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
defpred S₁[ Nat] means ( B . $1 <> 0 implies (A . 0) gcd (B . 0) = (A . $1) gcd (B . $1) );
A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) )

proof

assume A5: B . (i + 1) <> 0 ; :: thesis: (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1))
B . i <> 0

proof

assume A6: B . i = 0 ; :: thesis: contradiction
B . (i + 1) = (A . i) mod (B . i) by A1;
hence contradiction by A5, A6, INT_1:def 10; :: thesis: verum

end;

hence (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) by A4, A1, Lm3; :: thesis: verum

end;

hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for i being Nat st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; :: thesis: verum