scheme :: FRIENDS1:sch 1
Sch{ F₁() -> non empty set , F₂() -> non zero Nat, P₁[ set ] } :

ex C being Cardinal st F₂() *` C = card { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }

provided

A1: for p, q being FinSequence of F₁() st p ^ q is F₂() -element & P₁[p ^ q] holds
P₁[q ^ p] and
A2: for p being Element of F₂() -tuples_on F₁() st P₁[p] holds
for i being Nat st i < F₂() & p = (p /^ i) ^ (p | i) holds
i = 0