let a, b be Integer; :: thesis: for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds

( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being 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 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds

( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds

( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) implies ( A1 = A2 & B1 = B2 ) )

assume A1: ( A1 . 0 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds

( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) ) ; :: thesis: ( not A2 . 0 = |.a.| or not B2 . 0 = |.b.| or ex i being Nat st

( A2 . (i + 1) = B2 . i implies not B2 . (i + 1) = (A2 . i) mod (B2 . i) ) or ( A1 = A2 & B1 = B2 ) )

assume A2: ( A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds

( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) ) ; :: thesis: ( A1 = A2 & B1 = B2 )

defpred S_{1}[ Nat] means ( A1 . $1 = A2 . $1 & B1 . $1 = B2 . $1 );

A3: S_{1}[ 0 ]
by A1, A2;

A4: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A3, A4);

hence ( A1 = A2 & B1 = B2 ) ; :: thesis: verum

( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being 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 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds

( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds

( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) implies ( A1 = A2 & B1 = B2 ) )

assume A1: ( A1 . 0 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds

( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) ) ; :: thesis: ( not A2 . 0 = |.a.| or not B2 . 0 = |.b.| or ex i being Nat st

( A2 . (i + 1) = B2 . i implies not B2 . (i + 1) = (A2 . i) mod (B2 . i) ) or ( A1 = A2 & B1 = B2 ) )

assume A2: ( A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds

( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) ) ; :: thesis: ( A1 = A2 & B1 = B2 )

defpred S

A3: S

A4: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

A6: A1 . (n + 1) = B1 . n by A1

.= A2 . (n + 1) by A2, A5 ;

B1 . (n + 1) = (A1 . n) mod (B1 . n) by A1

.= B2 . (n + 1) by A2, A5 ;

hence S_{1}[n + 1]
by A6; :: thesis: verum

end;assume A5: S

A6: A1 . (n + 1) = B1 . n by A1

.= A2 . (n + 1) by A2, A5 ;

B1 . (n + 1) = (A1 . n) mod (B1 . n) by A1

.= B2 . (n + 1) by A2, A5 ;

hence S

hence ( A1 = A2 & B1 = B2 ) ; :: thesis: verum