let R1, R2 be Relation of (I *); :: thesis: ( ( for p, q being I -valued FinSequence holds
( [p,q] in R1 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 ) ) ) ) ) & ( for p, q being I -valued FinSequence holds
( [p,q] in R2 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 ) ) ) ) ) implies R1 = R2 )
assume that
A1: for p, q being I -valued FinSequence holds
( [p,q] in R1 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 ) ) ) ) and
A2: for p, q being I -valued FinSequence holds
( [p,q] in R2 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 ) ) ) ) ; :: thesis: R1 = R2
let p, q be Element of I * ; :: according to RELSET_1:def 2 :: thesis: ( ( not [p,q] in R1 or [p,q] in R2 ) & ( not [p,q] in R2 or [p,q] in R1 ) )
( [p,q] in R1 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 ) ) ) ) by A1;
hence ( ( not [p,q] in R1 or [p,q] in R2 ) & ( not [p,q] in R2 or [p,q] in R1 ) ) by A2; :: thesis: verum