defpred S₁[ object ] means ex a being FinSequence 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();
X is FinSequence-membered

proof

let x be object ; :: according to FINSEQ_1:def 19 :: thesis: ( not x in X or x is set )
assume x in X ; :: thesis: x is set
then ex a being FinSequence st
( P₁[a] & x = a ) by A2;
hence x is set ; :: thesis: verum

end;

then reconsider X = X as FinSequence-membered set ;
X is with_common_domain

proof

let a be FinSequence; :: according to MARGREL1:def 1 :: thesis: for b being FinSequence st a in X & b in X holds
len a = len b
let b be FinSequence; :: 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 st
( P₁[d] & b = d ) by A2, A4;
ex c being FinSequence st
( P₁[c] & a = c ) by A2, A3;
hence len a = len b by A1, A5; :: thesis: verum

end;

then reconsider r = X as relation ;
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 :: thesis: ( a in r implies ( a in F₁() & P₁[a] ) )

assume A6: 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, A6; :: 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