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 S1[ Nat] means ( B . \$1 <> 0 implies (A . 0) gcd (B . 0) = (A . \$1) gcd (B . \$1) );
A2: S1[ 0 ] ;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; :: thesis: S1[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 S1[i + 1] ; :: thesis: verum
end;
for i being Nat holds S1[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