defpred S1[ object ] means ex a being FinSequence of F1() st
( len a = F2() & P1[a] & $1 = a );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in F1() * & S1[x] ) ) from XBOOLE_0:sch 1();
 A2: for a, b being FinSequence of F1() st a in X & b in X holds
len a = len b
proof
let a, b be FinSequence of F1(); :: 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 F1() st
( len d = F2() & P1[d] & b = d ) by A1, A4;
ex c being FinSequence of F1() st
( len c = F2() & P1[c] & a = c ) by A1, A3;
hence len a = len b by A5; :: thesis: verum
end;
for x being object st x in X holds
x in F1() * by A1;
then X c= F1() * ;
then reconsider r = X as Element of relations_on F1() by A2, Def7;
for a being FinSequence of F1() st len a = F2() holds
( a in r iff P1[a] )
proof
let a be FinSequence of F1(); :: thesis: ( len a = F2() implies ( a in r iff P1[a] ) )
assume A6: len a = F2() ; :: thesis: ( a in r iff P1[a] )
A7: now :: thesis: ( P1[a] implies a in r )
A8: a in F1() * by FINSEQ_1:def 11;
assume P1[a] ; :: thesis: a in r
hence a in r by A1, A6, A8; :: thesis: verum
end;
now :: thesis: ( a in r implies P1[a] )
assume a in r ; :: thesis: P1[a]
then ex c being FinSequence of F1() st
( len c = F2() & P1[c] & a = c ) by A1;
hence P1[a] ; :: thesis: verum
end;
hence ( a in r iff P1[a] ) by A7; :: thesis: verum
end;
hence ex r being Element of relations_on F1() st
for a being FinSequence of F1() st len a = F2() holds
( a in r iff P1[a] ) ; :: thesis: verum