scheme :: FRECHET2:sch 1
PermSeq{ F₁() -> non empty 1-sorted , F₂() -> sequence of F₁(), F₃() -> Permutation of NAT, P₁[ set ] } :

ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P₁[(F₂() * F₃()) . m]

provided

A1: ex n being Element of NAT st
for m being Element of NAT
for x being Point of F₁() st n <= m & x = F₂() . m holds
P₁[x]