defpred S₁[ object ] means ex a being FinSequence of F₁() st
( P₁[a] & $1 = a );
consider X being set such that
A2: for x being object holds
( x in X iff ( x in F₁() * & S₁[x] ) ) from XBOOLE_0:sch 1();
A3: for a, b being FinSequence of F₁() st a in X & b in X holds
len a = len b

proof

let a, b be FinSequence of F₁(); :: thesis: ( a in X & b in X implies len a = len b )
assume that
A4: a in X and
A5: b in X ; :: thesis: len a = len b
A6: ex d being FinSequence of F₁() st
( P₁[d] & b = d ) by A2, A5;
ex c being FinSequence of F₁() st
( P₁[c] & a = c ) by A2, A4;
hence len a = len b by A1, A6; :: thesis: verum

end;

for x being object st x in X holds
x in F₁() * by A2;
then X c= F₁() * ;
then reconsider r = X as Element of relations_on F₁() by A3, Def7;
for a being FinSequence of F₁() holds
( a in r iff P₁[a] )

proof

let a be FinSequence of F₁(); :: thesis: ( a in r iff P₁[a] )

A7: now :: thesis: ( P₁[a] implies a in r )

A8: a in F₁() * by FINSEQ_1:def 11;
assume P₁[a] ; :: thesis: a in r
hence a in r by A2, A8; :: thesis: verum

end;

now :: thesis: ( a in r implies P₁[a] )

assume a in r ; :: thesis: P₁[a]
then ex c being FinSequence of F₁() st
( P₁[c] & a = c ) by A2;
hence P₁[a] ; :: thesis: verum

end;

hence ( a in r iff P₁[a] ) by A7; :: thesis: verum

end;

hence ex r being Element of relations_on F₁() st
for a being FinSequence of F₁() holds
( a in r iff P₁[a] ) ; :: thesis: verum