scheme :: MARGREL1:sch 3
relDexist2{ F1() -> non empty set , F2() -> Element of NAT , P1[ FinSequence of F1()] } :
ex r being Element of relations_on F1() st
for a being FinSequence of F1() st len a = F2() holds
( a in r iff P1[a] )