let a, b be Element of INT ; :: thesis: for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds
( A1 = A2 & B1 = B2 )
let A1, B1, A2, B2 be sequence of NAT; :: thesis: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) implies ( A1 = A2 & B1 = B2 ) )
assume P1: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) ) ; :: thesis: ( not A2 . 0 = abs a or not B2 . 0 = abs b or ex i being Element of NAT st
( A2 . (i + 1) = B2 . i implies not B2 . (i + 1) = (A2 . i) mod (B2 . i) ) or ( A1 = A2 & B1 = B2 ) )
assume P2: ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) ) ; :: thesis: ( A1 = A2 & B1 = B2 )
defpred S₁[ Nat] means ( A1 . $1 = A2 . $1 & B1 . $1 = B2 . $1 );
P0: S₁[ 0 ] by P1, P2;
PN: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume PN1: S₁[n] ; :: thesis: S₁[n + 1]
PN2: A1 . (n + 1) = B1 . n by P1
.= A2 . (n + 1) by P2, PN1 ;
B1 . (n + 1) = (A1 . n) mod (B1 . n) by P1
.= B2 . (n + 1) by P2, PN1 ;
hence S₁[n + 1] by PN2; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(P0, PN);
hence ( A1 = A2 & B1 = B2 ) by FUNCT_2:def 8; :: thesis: verum