let a, b be Integer; :: thesis: ex 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) ) ) )

defpred S_{1}[ Nat, Nat, Nat, Nat, Nat] means ( $4 = $3 & $5 = $2 mod $3 );

A1: for n being Nat

for x, y being Element of NAT ex x1, y1 being Element of NAT st S_{1}[n,x,y,x1,y1]
;

consider A, B being sequence of NAT such that

A2: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for n being Nat holds S_{1}[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) )
from RECDEF_2:sch 3(A1);

take A ; :: thesis: ex 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) ) ) )

take B ; :: 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) ) ) )

thus ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by A2; :: thesis: verum

( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )

defpred S

A1: for n being Nat

for x, y being Element of NAT ex x1, y1 being Element of NAT st S

consider A, B being sequence of NAT such that

A2: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for n being Nat holds S

take A ; :: thesis: ex 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) ) ) )

take B ; :: 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) ) ) )

thus ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by A2; :: thesis: verum