per cases ( A is empty or not A is empty ) ;

suppose A2: A is empty ; :: thesis: ex b₁ being FinSequence of X st
( rng b₁ = A & ( for n, m being Nat st n in dom b₁ & m in dom b₁ & n < m holds
( b₁ /. n <> b₁ /. m & [(b₁ /. n),(b₁ /. m)] in R ) ) )

take <*> X ; :: thesis: ( rng (<*> X) = A & ( for n, m being Nat st n in dom (<*> X) & m in dom (<*> X) & n < m holds
( (<*> X) /. n <> (<*> X) /. m & [((<*> X) /. n),((<*> X) /. m)] in R ) ) )
thus ( rng (<*> X) = A & ( for n, m being Nat st n in dom (<*> X) & m in dom (<*> X) & n < m holds
( (<*> X) /. n <> (<*> X) /. m & [((<*> X) /. n),((<*> X) /. m)] in R ) ) ) by A2; :: thesis: verum

end;

suppose A3: not A is empty ; :: thesis: ex b₁ being FinSequence of X st
( rng b₁ = A & ( for n, m being Nat st n in dom b₁ & m in dom b₁ & n < m holds
( b₁ /. n <> b₁ /. m & [(b₁ /. n),(b₁ /. m)] in R ) ) )

then reconsider X9 = X as non empty set ;
reconsider A1 = A as non empty finite Subset of X9 by A3;
reconsider R9 = R as Order of X9 ;
deffunc H₁( set ) -> set = $1;
deffunc H₂( Element of A1) -> set = { H₁(x) where x is Element of A1 : ( x <=_ R9,$1 & x <> $1 ) } ;
deffunc H₃( Element of A1) -> set = (card H₂($1)) +^ 1;
X: for x being Element of A1 holds H₃(x) is Element of NAT

proof

let a be Element of A1; :: thesis: H₃(a) is Element of NAT
defpred S₁[ Element of A1] means ( $1 <=_ R9,a & $1 <> a );
{ H₁(x) where x is Element of A1 : S₁[x] } is finite from PRE_CIRC:sch 1();
then reconsider X = { H₁(x) where x is Element of A1 : S₁[x] } as finite set ;
reconsider n = card X as Element of NAT ;
n +^ 1 = n + 1 by CARD_2:49;
hence H₃(a) is Element of NAT ; :: thesis: verum

end;

consider f being Function of A1,NAT such that
A5: for x being Element of A1 holds f . x = H₃(x) from FUNCT_2:sch 9(X);
O62: for x being Element of A1 holds not x in H₂(x)

proof

let a be Element of A1; :: thesis: not a in H₂(a)
assume a in H₂(a) ; :: thesis: contradiction
then ex x being Element of A1 st
( x = a & x <=_ R9,a & x <> a ) ;
hence contradiction ; :: thesis: verum

end;

XX: for x being Element of A1 holds H₂(x) c= A1

proof

let a be Element of A1; :: thesis: H₂(a) c= A1
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in H₂(a) or y in A1 )
assume y in H₂(a) ; :: thesis: y in A1
then ex x being Element of A1 st
( x = y & x <=_ R9,a & x <> a ) ;
hence y in A1 ; :: thesis: verum

end;

rng f c= Seg (card A1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Seg (card A1) )
assume y in rng f ; :: thesis: y in Seg (card A1)
then consider x1 being set such that
A6: x1 in dom f and
A7: y = f . x1 by FUNCT_1:def 5;
reconsider y1 = y as Nat by A7;
reconsider x2 = x1 as Element of A1 by A6;
defpred S₁[ Element of A1] means ( $1 <=_ R9,x2 & $1 <> x2 );
{ H₁(x) where x is Element of A1 : S₁[x] } is finite from PRE_CIRC:sch 1();
then reconsider Vx2 = H₂(x2) as finite set ;
Vx2 <> A1 by O62;
then y: card Vx2 <> card A1 by XX, Th3;
card Vx2 <= card A1 by NAT_1:44, XX;
then card Vx2 < card A1 by y, XXREAL_0:1;
then A9: (card Vx2) + 1 <= card A1 by NAT_1:13;
A10: y = (card Vx2) +^ 1 by A5, A7
.= (card Vx2) + 1 by CARD_2:49 ;
then 0 + 1 <= y1 by XREAL_1:8;
hence y in Seg (card A1) by A9, A10, FINSEQ_1:3; :: thesis: verum

end;

then reconsider f1 = f as Function of A1,(Seg (card A1)) by FUNCT_2:8;
A4: R |_2 A c= R by XBOOLE_1:17;
B11: R is_connected_in A by A1, ORDERS_1:def 8;
then A11: R |_2 A is connected by ORDERS_1:185;
field (R9 |_2 A1) = A by ORDERS_1:100;
then A12: R |_2 A is_connected_in A by A11, RELAT_2:def 14;
D12: R9 is_transitive_in A by A1, ORDERS_1:def 8;
D13: R9 is_antisymmetric_in A by A1, ORDERS_1:def 8;
for x1, x2 being set st x1 in A1 & x2 in A1 & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in A1 & x2 in A1 & f . x1 = f . x2 implies x1 = x2 )
assume that
A13: x1 in A1 and
A14: x2 in A1 and
A15: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x29 = x2 as Element of A1 by A14;
reconsider x19 = x1 as Element of A1 by A13;
defpred S₁[ Element of A1] means ( $1 <=_ R9,x19 & $1 <> x19 );
{ H₁(x) where x is Element of A1 : S₁[x] } is finite from PRE_CIRC:sch 1();
then reconsider Vx1 = H₂(x19) as finite set ;
defpred S₂[ Element of A1] means ( $1 <=_ R9,x29 & $1 <> x29 );
{ H₁(x) where x is Element of A1 : S₂[x] } is finite from PRE_CIRC:sch 1();
then reconsider Vx2 = H₂(x29) as finite set ;
XX1: for x1, x2 being Element of A1 st x1 <=_ R |_2 A,x2 holds
H₂(x1) c= H₂(x2)

proof

let x1, x2 be Element of A1; :: thesis: ( x1 <=_ R |_2 A,x2 implies H₂(x1) c= H₂(x2) )
assume x1 <=_ R |_2 A,x2 ; :: thesis: H₂(x1) c= H₂(x2)
then z: [x1,x2] in R |_2 A by ARROW:def 4;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H₂(x1) or x in H₂(x2) )
assume x in H₂(x1) ; :: thesis: x in H₂(x2)
then consider a being Element of A such that
W1: a = x and
W2: a <=_ R9,x1 and
W3: a <> x1 ;
xx: [a,x1] in R9 by W2, ARROW:def 4;
then [a,x2] in R9 by z, A4, RELAT_2:def 8, D12;
then A: a <=_ R9,x2 by ARROW:def 4;
a <> x2 by W3, xx, z, A4, D13, RELAT_2:def 4;
hence x in H₂(x2) by W1, A; :: thesis: verum

end;

f . x19 = (card Vx1) +^ 1 by A5
.= (card Vx1) + 1 by CARD_2:49 ;
then A16: (card Vx1) + 1 = (card Vx2) +^ 1 by A5, A15
.= (card Vx2) + 1 by CARD_2:49 ;

now

per cases ( x19 = x29 or x19 <> x29 ) ;

suppose x19 = x29 ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

suppose x19 <> x29 ; :: thesis: x1 = x2

then C18: ( [x19,x29] in R |_2 A or [x29,x19] in R |_2 A ) by A12, RELAT_2:def 6;
XX2: for x1, x2 being Element of A1 st x1 <> x2 & x1 <=_ R |_2 A,x2 holds
x1 in H₂(x2)

proof

let x1, x2 be Element of A1; :: thesis: ( x1 <> x2 & x1 <=_ R |_2 A,x2 implies x1 in H₂(x2) )
assume Z1: x1 <> x2 ; :: thesis: ( not x1 <=_ R |_2 A,x2 or x1 in H₂(x2) )
assume x1 <=_ R |_2 A,x2 ; :: thesis: x1 in H₂(x2)
then [x1,x2] in R |_2 A by ARROW:def 4;
then x1 <=_ R9,x2 by ARROW:def 4, A4;
hence x1 in H₂(x2) by Z1; :: thesis: verum

end;

A19: now

per cases ( x19 <=_ R |_2 A,x29 or x29 <=_ R |_2 A,x19 ) by C18, ARROW:def 4;

suppose x19 <=_ R |_2 A,x29 ; :: thesis: Vx1 = Vx2

hence Vx1 = Vx2 by A16, Th3, XX1; :: thesis: verum

end;

suppose x29 <=_ R |_2 A,x19 ; :: thesis: Vx1 = Vx2

hence Vx1 = Vx2 by A16, Th3, XX1; :: thesis: verum

end;

end;

end;

now

assume A20: x19 <> x29 ; :: thesis: contradiction
then C21: ( [x19,x29] in R |_2 A or [x29,x19] in R |_2 A ) by A12, RELAT_2:def 6;

per cases ( x19 <=_ R |_2 A,x29 or x29 <=_ R |_2 A,x19 ) by C21, ARROW:def 4;

suppose x19 <=_ R |_2 A,x29 ; :: thesis: contradiction

hence contradiction by A19, O62, A20, XX2; :: thesis: verum

end;

suppose x29 <=_ R |_2 A,x19 ; :: thesis: contradiction

hence contradiction by A19, O62, A20, XX2; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

then A22: f1 is one-to-one by FUNCT_2:25;
A23: for x1, x2 being Element of A1 st f . x1 < f . x2 holds
( x1 <=_ R9,x2 & x1 <> x2 )

proof

let x1, x2 be Element of A1; :: thesis: ( f . x1 < f . x2 implies ( x1 <=_ R9,x2 & x1 <> x2 ) )
defpred S₁[ Element of A1] means ( $1 <=_ R9,x1 & $1 <> x1 );
{ H₁(x) where x is Element of A1 : S₁[x] } is finite from PRE_CIRC:sch 1();
then reconsider Vx1 = H₂(x1) as finite set ;
defpred S₂[ Element of A1] means ( $1 <=_ R9,x2 & $1 <> x2 );
{ H₁(x) where x is Element of A1 : S₂[x] } is finite from PRE_CIRC:sch 1();
then reconsider Vx2 = H₂(x2) as finite set ;
assume A24: f . x1 < f . x2 ; :: thesis: ( x1 <=_ R9,x2 & x1 <> x2 )
P1: f . x1 = (card Vx1) +^ 1 by A5
.= (card Vx1) + 1 by CARD_2:49 ;
f . x2 = (card Vx2) +^ 1 by A5
.= (card Vx2) + 1 by CARD_2:49 ;
then A25: ((card Vx1) + 1) - 1 < ((card Vx2) + 1) - 1 by XREAL_1:11, P1, A24;
reconsider Cx2 = card Vx2 as Cardinal ;
reconsider Cx1 = card Vx1 as Cardinal ;
A26: card (card Vx2) = card Vx2 ;
card (card Vx1) = card Vx1 ;
then Cx1 in Cx2 by A26, A25, NAT_1:42;
then Vx2 \ Vx1 <> {} by CARD_2:4;
then consider a being set such that
A27: a in Vx2 \ Vx1 by XBOOLE_0:def 1;
A28: not a in Vx1 by A27, XBOOLE_0:def 5;
A29: a in Vx2 by A27;
Vx2 c= A1 by XX;
then reconsider a = a as Element of A1 by A29;
B31: ex x being Element of A1 st
( a = x & x <=_ R9,x2 & x <> x2 ) by A29;
then C31: [a,x2] in R9 by ARROW:def 4;

now

per cases ( not a <=_ R9,x1 or a = x1 ) by A28;

suppose not a <=_ R9,x1 ; :: thesis: ( x1 <=_ R9,x2 & x1 <> x2 )

then A32: not [a,x1] in R9 by ARROW:def 4;

now

per cases ( x1 = a or x1 <> a ) ;

suppose x1 = a ; :: thesis: ( x1 <=_ R9,x2 & x1 <> x2 )

hence ( x1 <=_ R9,x2 & x1 <> x2 ) by B31; :: thesis: verum

end;

suppose S: x1 <> a ; :: thesis: ( x1 <=_ R9,x2 & not x1 = x2 )

then A: [x1,a] in R9 by B11, A32, RELAT_2:def 6;
then [x1,x2] in R9 by C31, D12, RELAT_2:def 8;
hence x1 <=_ R9,x2 by ARROW:def 4; :: thesis: not x1 = x2
assume x1 = x2 ; :: thesis: contradiction
then a = x1 by A, C31, D13, RELAT_2:def 4;
hence contradiction by S; :: thesis: verum

end;

end;

end;

hence ( x1 <=_ R9,x2 & x1 <> x2 ) ; :: thesis: verum

end;

suppose a = x1 ; :: thesis: ( x1 <=_ R9,x2 & x1 <> x2 )

hence ( x1 <=_ R9,x2 & x1 <> x2 ) by B31; :: thesis: verum

end;

end;

end;

hence ( x1 <=_ R9,x2 & x1 <> x2 ) ; :: thesis: verum

end;

card (Seg (card A1)) = card A1 by FINSEQ_1:78;
then rng f1 = Seg (card A1) by A22, FINSEQ_4:78;
then dom (f1 " ) = Seg (card A1) by A22, FUNCT_1:55;
then reconsider g1 = f1 " as FinSequence by FINSEQ_1:def 2;
A33: dom f1 = A by FUNCT_2:def 1;
then A34: rng g1 = A by A22, FUNCT_1:55;
then reconsider g = g1 as FinSequence of X by FINSEQ_1:def 4;
take g ; :: thesis: ( rng g = A & ( for n, m being Nat st n in dom g & m in dom g & n < m holds
( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) ) )
thus rng g = A by A22, A33, FUNCT_1:55; :: thesis: for n, m being Nat st n in dom g & m in dom g & n < m holds
( g /. n <> g /. m & [(g /. n),(g /. m)] in R )
let n, m be Nat; :: thesis: ( n in dom g & m in dom g & n < m implies ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) )
assume that
A35: n in dom g and
A36: m in dom g and
A37: n < m ; :: thesis: ( g /. n <> g /. m & [(g /. n),(g /. m)] in R )
reconsider gn = g . n as Element of A1 by A34, A35, FUNCT_1:def 5;
n in rng f by A22, A35, FUNCT_1:55;
then A38: n = f . gn by A22, FUNCT_1:57;
reconsider gm = g . m as Element of A1 by A34, A36, FUNCT_1:def 5;
A39: gm = g /. m by A36, PARTFUN1:def 8;
A40: m in rng f by A22, A36, FUNCT_1:55;
then m = f . gm by A22, FUNCT_1:57;
then gn <=_ R9,gm by A23, A37, A38;
then [gn,gm] in R by ARROW:def 4;
then A41: [gn,gm] in R |_2 A by XBOOLE_0:def 4;
gn = g /. n by A35, PARTFUN1:def 8;
hence ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) by A22, A37, A40, A38, A4, A41, A39, FUNCT_1:57; :: thesis: verum

end;

end;