let I be set ; :: thesis: for R being asymmetric transitive Relation of I
for r being RedSequence of R holds r is one-to-one
let R be asymmetric transitive Relation of I; :: thesis: for r being RedSequence of R holds r is one-to-one
let r be RedSequence of R; :: thesis: r is one-to-one
let a be object ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being object holds
( not a in dom r or not b₁ in dom r or not r . a = r . b₁ or a = b₁ )
let b be object ; :: thesis: ( not a in dom r or not b in dom r or not r . a = r . b or a = b )
assume Z0: ( a in dom r & b in dom r ) ; :: thesis: ( not r . a = r . b or a = b )
then reconsider i = a, j = b as Nat ;
assume Z1: ( r . a = r . b & a <> b ) ; :: thesis: contradiction
A1: for i, j being Nat st i > j & i in dom r & j in dom r holds
r . i <> r . j

proof

let i, j be Nat; :: thesis: ( i > j & i in dom r & j in dom r implies r . i <> r . j )
assume i > j ; :: thesis: ( not i in dom r or not j in dom r or r . i <> r . j )
then A1: i >= j + 1 by NAT_1:13;
assume Z3: i in dom r ; :: thesis: ( not j in dom r or r . i <> r . j )
assume Z4: j in dom r ; :: thesis: r . i <> r . j
defpred S₁[ Nat] means ( $1 in dom r implies ( [(r . j),(r . $1)] in R & r . $1 <> r . j ) );
A2: S₁[j + 1]

proof

assume j + 1 in dom r ; :: thesis: ( [(r . j),(r . (j + 1))] in R & r . (j + 1) <> r . j )
hence [(r . j),(r . (j + 1))] in R by Z4, REWRITE1:def 2; :: thesis: r . (j + 1) <> r . j
hence r . (j + 1) <> r . j by PREFER_1:22; :: thesis: verum

end;

A3: for i being Nat st i >= j + 1 & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( i >= j + 1 & S₁[i] implies S₁[i + 1] )
assume Z5: ( i >= j + 1 & S₁[i] & i + 1 in dom r ) ; :: thesis: ( [(r . j),(r . (i + 1))] in R & r . (i + 1) <> r . j )
then ( 1 <= j + 1 & i < i + 1 & i + 1 <= len r ) by NAT_1:11, NAT_1:13, FINSEQ_3:25;
then ( 1 <= i & i <= len r ) by Z5, XXREAL_0:2;
then i in dom r by FINSEQ_3:25;
then ZZ: ( [(r . j),(r . i)] in R & [(r . i),(r . (i + 1))] in R ) by Z5, REWRITE1:def 2;
hence [(r . j),(r . (i + 1))] in R by RELAT_2:31; :: thesis: r . (i + 1) <> r . j
thus r . (i + 1) <> r . j by PREFER_1:22, ZZ; :: thesis: verum

end;

for i being Nat st i >= j + 1 holds
S₁[i] from NAT_1:sch 8(A2, A3);
hence r . i <> r . j by A1, Z3; :: thesis: verum

end;

( i < j or j < i ) by Z1, XXREAL_0:1;
hence contradiction by Z0, Z1, A1; :: thesis: verum