defpred S₁[ object , object ] means for a, b being FinSequence of D st a = $1 & b = $2 holds
( len a = len b & ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R ) );
consider P being Relation of (D *),(D *) such that
A1: for x, y being object holds
( [x,y] in P iff ( x in D * & y in D * & S₁[x,y] ) ) from RELSET_1:sch 1();
take P ; :: thesis: for x, y being FinSequence of D holds
( [x,y] in P iff ( len x = len y & ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R ) ) )
let a, b be FinSequence of D; :: thesis: ( [a,b] in P iff ( len a = len b & ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R ) ) )
thus ( [a,b] in P implies ( len a = len b & ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R ) ) ) by A1; :: thesis: ( len a = len b & ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R ) implies [a,b] in P )
assume ( len a = len b & ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R ) ) ; :: thesis: [a,b] in P
then A2: S₁[a,b] ;
( a in D * & b in D * ) by FINSEQ_1:def 11;
hence [a,b] in P by A1, A2; :: thesis: verum