defpred S₁[ set , set ] means for a, b being FinSequence of D st a = $1 & b = $2 holds
( len a = len b & ( for n being Element of 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 set 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 Element of 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 Element of 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 Element of NAT st n in dom a holds
[(a . n),(b . n)] in R ) ) ) by A1; :: thesis: ( len a = len b & ( for n being Element of NAT st n in dom a holds
[(a . n),(b . n)] in R ) implies [a,b] in P )
assume A2: ( len a = len b & ( for n being Element of NAT st n in dom a holds
[(a . n),(b . n)] in R ) ) ; :: thesis: [a,b] in P
A3: ( a in D * & b in D * ) by FINSEQ_1:def 11;
S₁[a,b] by A2;
hence [a,b] in P by A1, A3; :: thesis: verum