let f1, f2 be XFinSequence of X; ( 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 ) ) )
; 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
; contradiction
then consider x being object such that
A11:
( x in dom f1 & f1 . x <> f2 . x )
by A10;
defpred S1[ Nat] means ( $1 in dom f1 & f1 . $1 <> f2 . $1 );
A12:
ex n being Nat st S1[n]
by A11;
consider n being Nat such that
A13:
( S1[n] & ( for m being Nat st S1[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;
now not b < nassume
b < n
;
contradictionthen
f1 . b = f2 . b
by A13, A15;
hence
contradiction
by A9, A10, A13, A15;
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; verum