scheme :: MATRIX_9:sch 1
NonEmptyFiniteX{ F₁() -> Element of NAT , F₂() -> non empty Element of Fin (Permutations F₁()), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x being Element of Permutations F₁() st x in F₂() holds
P₁[{x}] and
A2: for x being Element of Permutations F₁()
for B being non empty Element of Fin (Permutations F₁()) st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[B \/ {x}]