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

proof

let x be set ; :: thesis: ( x in X implies x is FinSequence )
assume x in X ; :: thesis: x is FinSequence
then ex a being FinSequence st
( P₁[a] & x = a ) by A2;
hence x is FinSequence ; :: thesis: verum

end;

for a, b being FinSequence st a in X & b in X holds
len a = len b

proof

let a, b be FinSequence; :: 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 c being FinSequence st
( P₁[c] & a = c ) by A2, A4;
ex d being FinSequence st
( P₁[d] & b = d ) by A2, A5;
hence len a = len b by A1, A6; :: thesis: verum

end;

then reconsider r = X as relation by A3, Def1;
for a being FinSequence holds
( a in r iff ( a in F₁() & P₁[a] ) )

proof

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

now

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

end;

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

end;

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