scheme :: NEWTON:sch 1
Euklides9{ F₁( Nat) -> Element of NAT , F₂( Nat) -> Element of NAT , F₃() -> Element of NAT , F₄() -> Element of NAT } :

ex k being Nat st
( F₁(k) = F₃() gcd F₄() & F₂(k) = 0 )

provided

A1: 0 < F₄() and
A2: F₄() < F₃() and
A3: F₁(0) = F₃() and
A4: F₂(0) = F₄() and
A5: for k being Nat st F₂(k) > 0 holds
( F₁((k + 1)) = F₂(k) & F₂((k + 1)) = F₁(k) mod F₂(k) )