scheme :: FIN_TOPO:sch 1
MaxFinSeqEx{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), F₄( Subset of F₁()) -> Subset of F₁() } :

ex f being FinSequence of bool F₁() st
( len f > 0 & f /. 1 = F₃() & ( for i being Nat st i > 0 & i < len f holds
f /. (i + 1) = F₄((f /. i)) ) & F₄((f /. (len f))) = f /. (len f) & ( for i, j being Nat st i > 0 & i < j & j <= len f holds
( f /. i c= F₂() & f /. i c< f /. j ) ) )

provided

A1: F₂() is finite and
A2: F₃() c= F₂() and
A3: for A being Subset of F₁() st A c= F₂() holds
( A c= F₄(A) & F₄(A) c= F₂() )