scheme :: PENCIL_2:sch 1
FinSeqOneToOne{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> FinSequence of F₃(), P₁[ set , set ] } :

ex g being one-to-one FinSequence of F₃() st
( F₁() = g . 1 & F₂() = g . (len g) & rng g c= rng F₄() & ( for j being Element of NAT st 1 <= j & j < len g holds
P₁[g . j,g . (j + 1)] ) )

provided

A1: ( F₁() = F₄() . 1 & F₂() = F₄() . (len F₄()) ) and
A2: for i being Element of NAT
for d1, d2 being set st 1 <= i & i < len F₄() & d1 = F₄() . i & d2 = F₄() . (i + 1) holds
P₁[d1,d2]