scheme :: MARGREL1:sch 3
relDexist2{ F₁() -> non empty set , F₂() -> Element of NAT , P₁[ FinSequence of F₁()] } :

ex r being Element of relations_on F₁() st
for a being FinSequence of F₁() st len a = F₂() holds
( a in r iff P₁[a] )