defpred S₁[ set ] means ex a being FinSequence of F₁() st
( len a = F₂() & P₁[a] & $1 = a );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in F₁() * & S₁[x] ) ) from XBOOLE_0:sch 1();
A2: 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
A3: a in X and
A4: b in X ; :: thesis: len a = len b
A5: ex d being FinSequence of F₁() st
( len d = F₂() & P₁[d] & b = d ) by A1, A4;
ex c being FinSequence of F₁() st
( len c = F₂() & P₁[c] & a = c ) by A1, A3;
hence len a = len b by A5; :: thesis: verum

end;

for x being set st x in X holds
x in F₁() * by A1;
then X c= F₁() * by TARSKI:def 3;
then reconsider r = X as Element of relations_on F₁() by A2, Def8;
for a being FinSequence of F₁() st len a = F₂() holds
( a in r iff P₁[a] )

proof

let a be FinSequence of F₁(); :: thesis: ( len a = F₂() implies ( a in r iff P₁[a] ) )
assume A6: len a = F₂() ; :: thesis: ( a in r iff P₁[a] )

A7: now

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

end;

now

assume a in r ; :: thesis: P₁[a]
then ex c being FinSequence of F₁() st
( len c = F₂() & P₁[c] & a = c ) by A1;
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₁() st len a = F₂() holds
( a in r iff P₁[a] ) ; :: thesis: verum