defpred S₁[ Element of I * , Element of I * ] means ( $1 c< $2 or ex k being Nat st
( k in dom $1 & k in dom $2 & [($1 . k),($2 . k)] in R & ( for n being Nat st 1 <= n & n < k holds
$1 . n = $2 . n ) ) );
consider R being Relation of (I *) such that
A1: for b1, b2 being Element of I * holds
( [b1,b2] in R iff S₁[b1,b2] ) from RELSET_1:sch 2();
take R ; :: thesis: for p, q being I -valued FinSequence holds
( [p,q] in R iff ( p c< q or ex k being Nat st
( k in dom p & k in dom q & [(p . k),(q . k)] in R & ( for n being Nat st 1 <= n & n < k holds
p . n = q . n ) ) ) )
let b1, b2 be I -valued FinSequence; :: thesis: ( [b1,b2] in R iff ( b1 c< b2 or ex k being Nat st
( k in dom b1 & k in dom b2 & [(b1 . k),(b2 . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b1 . n = b2 . n ) ) ) )
( rng b1 c= I & rng b2 c= I ) by RELAT_1:def 19;
then ( b1 is FinSequence of I & b2 is FinSequence of I ) by FINSEQ_1:def 4;
then ( b1 in I * & b2 in I * ) by FINSEQ_1:def 11;
hence ( [b1,b2] in R iff ( b1 c< b2 or ex k being Nat st
( k in dom b1 & k in dom b2 & [(b1 . k),(b2 . k)] in R & ( for n being Nat st 1 <= n & n < k holds
b1 . n = b2 . n ) ) ) ) by A1; :: thesis: verum