scheme :: MARGREL1:sch 1
relexist{ F1() -> set , P1[ FinSequence] } :
ex r being relation st
for a being FinSequence holds
( a in r iff ( a in F1() & P1[a] ) )
provided
A1: for a, b being FinSequence st P1[a] & P1[b] holds
len a = len b