defpred S1[ object ] means ex a being FinSequence st
( P1[a] & $1 = a );
consider X being set such that
A2: for x being object holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch 1();
 X is FinSequence-membered
proof
let x be object ; :: according to FINSEQ_1:def 18 :: thesis: ( not x in X or x is set )
assume x in X ; :: thesis: x is set
then ex a being FinSequence st
( P1[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
( P1[d] & b = d ) by A2, A4;
ex c being FinSequence st
( P1[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 F1() & P1[a] ) )
proof
let a be FinSequence; :: thesis: ( a in r iff ( a in F1() & P1[a] ) )
now :: thesis: ( a in r implies ( a in F1() & P1[a] ) )
assume A6: a in r ; :: thesis: ( a in F1() & P1[a] )
then ex c being FinSequence st
( P1[c] & a = c ) by A2;
hence ( a in F1() & P1[a] ) by A2, A6; :: thesis: verum
end;
hence ( a in r iff ( a in F1() & P1[a] ) ) by A2; :: thesis: verum
end;
hence ex r being relation st
for a being FinSequence holds
( a in r iff ( a in F1() & P1[a] ) ) ; :: thesis: verum