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)] ) )

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]