let f1, f2 be XFinSequence of X; :: thesis: ( rng f1 = S & f1 is one-to-one & ( for i, j being Nat st i in dom f1 & j in dom f1 holds
( i <= j iff f1 . i,f1 . j in R ) ) & rng f2 = S & f2 is one-to-one & ( for i, j being Nat st i in dom f2 & j in dom f2 holds
( i <= j iff f2 . i,f2 . j in R ) ) implies f1 = f2 )
assume that
A8: ( rng f1 = S & f1 is one-to-one & ( for i, j being Nat st i in dom f1 & j in dom f1 holds
( i <= j iff f1 . i,f1 . j in R ) ) ) and
A9: ( rng f2 = S & f2 is one-to-one & ( for i, j being Nat st i in dom f2 & j in dom f2 holds
( i <= j iff f2 . i,f2 . j in R ) ) ) ; :: thesis: f1 = f2
( dom f1,S are_equipotent & dom f2,S are_equipotent ) by A8, A9, WELLORD2:def 4;
then dom f1, dom f2 are_equipotent by WELLORD2:15;
then card (dom f1) = dom f2 by CARD_1:def 2;
then A10: dom f1 = dom f2 ;
assume f1 <> f2 ; :: thesis: contradiction
then consider x being object such that
A11: ( x in dom f1 & f1 . x <> f2 . x ) by A10;
defpred S₁[ Nat] means ( $1 in dom f1 & f1 . $1 <> f2 . $1 );
A12: ex n being Nat st S₁[n] by A11;
consider n being Nat such that
A13: ( S₁[n] & ( for m being Nat st S₁[m] holds
n <= m ) ) from NAT_1:sch 5(A12);
f1 . n in S by A8, A13, FUNCT_1:def 3;
then consider a being object such that
A14: ( a in dom f2 & f1 . n = f2 . a ) by A9, FUNCT_1:def 3;
f2 . n in S by A9, A10, A13, FUNCT_1:def 3;
then consider b being object such that
A15: ( b in dom f1 & f2 . n = f1 . b ) by A8, FUNCT_1:def 3;
reconsider a = a, b = b as Element of NAT by A14, A15;

A16: now :: thesis: not a < n

assume a < n ; :: thesis: contradiction
then f1 . a = f2 . a by A10, A13, A14;
hence contradiction by A8, A10, A13, A14; :: thesis: verum

end;

now :: thesis: not b < n

assume b < n ; :: thesis: contradiction
then f1 . b = f2 . b by A13, A15;
hence contradiction by A9, A10, A13, A15; :: thesis: verum

end;

then ( f1 . n,f1 . b in R & f2 . n,f2 . a in R ) by A8, A9, A10, A13, A14, A15, A16;
hence contradiction by A13, A14, A15, Def2; :: thesis: verum