scheme :: AOFA_A01:sch 1
Sch1{ F₁() -> non empty set , F₂() -> Nat, F₃() -> set , F₄( set , set , set ) -> set , F₅( set ) -> set } :

ex f being FinSequence of F₁() ^omega st
( len f = F₂() & ( f . 1 = F₃() or F₂() = 0 ) & ( for i being Nat st 1 <= i & i < F₂() holds
f . (i + 1) = F₄((f . i),i,F₅(i)) ) )

provided

A1: for a being finite 0 -based array of F₁()
for i being Nat st 1 <= i & i < F₂() holds
for x being Element of F₁() holds F₄(a,i,x) is finite 0 -based array of F₁() and
A2: F₃() is finite 0 -based array of F₁() and
A3: for i being Nat st i < F₂() holds
F₅(i) in F₁()