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;
A4: 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:36;
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(A4);
A6: 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;

A7: 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 object ; :: 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 object ; :: 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 object such that
A8: x1 in dom f and
A9: y = f . x1 by FUNCT_1:def 3;
reconsider y1 = y as Nat by A9;
reconsider x2 = x1 as Element of A1 by A8;
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 A6;
then A10: card Vx2 <> card A1 by A7, CARD_2:102;
card Vx2 <= card A1 by A7, NAT_1:43;
then card Vx2 < card A1 by A10, XXREAL_0:1;
then A11: (card Vx2) + 1 <= card A1 by NAT_1:13;
A12: y = (card Vx2) +^ 1 by A5, A9
.= (card Vx2) + 1 by CARD_2:36 ;
then 0 + 1 <= y1 by XREAL_1:6;
hence y in Seg (card A1) by A11, A12, FINSEQ_1:1; :: thesis: verum

end;

then reconsider f1 = f as Function of A1,(Seg (card A1)) by FUNCT_2:6;
A13: R |_2 A c= R by XBOOLE_1:17;
A14: R is_connected_in A by A1, ORDERS_1:def 9;
then A15: R |_2 A is connected by ORDERS_1:75;
A16: field (R9 |_2 A1) = A by ORDERS_1:15;
A17: R9 is_transitive_in A by A1, ORDERS_1:def 9;
A18: R9 is_antisymmetric_in A by A1, ORDERS_1:def 9;
for x1, x2 being object st x1 in A1 & x2 in A1 & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in A1 & x2 in A1 & f . x1 = f . x2 implies x1 = x2 )
assume that
A19: x1 in A1 and
A20: x2 in A1 and
A21: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x29 = x2 as Element of A1 by A20;
reconsider x19 = x1 as Element of A1 by A19;
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 ;
A22: 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 A23: [x1,x2] in R |_2 A by ARROW:def 4;
let x be object ; :: 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
A24: a = x and
A25: a <=_ R9,x1 and
A26: a <> x1 ;
A27: [a,x1] in R9 by A25, ARROW:def 4;
then [a,x2] in R9 by A23, A13, A17;
then A28: a <=_ R9,x2 by ARROW:def 4;
a <> x2 by A26, A27, A23, A13, A18;
hence x in H₂(x2) by A24, A28; :: thesis: verum

end;

f . x19 = (card Vx1) +^ 1 by A5
.= (card Vx1) + 1 by CARD_2:36 ;
then A29: (card Vx1) + 1 = (card Vx2) +^ 1 by A5, A21
.= (card Vx2) + 1 by CARD_2:36 ;

now :: thesis: x1 = x2

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 A30: ( [x19,x29] in R |_2 A or [x29,x19] in R |_2 A ) by A16, A15, RELAT_2:def 6;
A31: 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 A32: 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 A13, ARROW:def 4;
hence x1 in H₂(x2) by A32; :: thesis: verum

end;

A33: now :: thesis: Vx1 = Vx2

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

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

hence Vx1 = Vx2 by A29, A22, CARD_2:102; :: thesis: verum

end;

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

hence Vx1 = Vx2 by A29, A22, CARD_2:102; :: thesis: verum

end;

end;

end;

now :: thesis: not x19 <> x29

assume A34: x19 <> x29 ; :: thesis: contradiction
then A35: ( [x19,x29] in R |_2 A or [x29,x19] in R |_2 A ) by A16, A15, RELAT_2:def 6;

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

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

hence contradiction by A33, A6, A34, A31; :: thesis: verum

end;

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

hence contradiction by A33, A6, A34, A31; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

then A36: f1 is one-to-one by FUNCT_2:19;
A37: 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 A38: f . x1 < f . x2 ; :: thesis: ( x1 <=_ R9,x2 & x1 <> x2 )
A39: f . x1 = (card Vx1) +^ 1 by A5
.= (card Vx1) + 1 by CARD_2:36 ;
f . x2 = (card Vx2) +^ 1 by A5
.= (card Vx2) + 1 by CARD_2:36 ;
then A40: ((card Vx1) + 1) - 1 < ((card Vx2) + 1) - 1 by A39, A38, XREAL_1:9;
reconsider Cx2 = card Vx2 as Cardinal ;
reconsider Cx1 = card Vx1 as Cardinal ;
A41: card (Segm (card Vx2)) = card Vx2 ;
card (Segm (card Vx1)) = card Vx1 ;
then Vx2 \ Vx1 <> {} by A41, A40, CARD_1:68, NAT_1:41;
then consider a being object such that
A42: a in Vx2 \ Vx1 by XBOOLE_0:def 1;
A43: not a in Vx1 by A42, XBOOLE_0:def 5;
A44: a in Vx2 by A42;
Vx2 c= A1 by A7;
then reconsider a = a as Element of A1 by A44;
A45: ex x being Element of A1 st
( a = x & x <=_ R9,x2 & x <> x2 ) by A44;
then A46: [a,x2] in R9 by ARROW:def 4;

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

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

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

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

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

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

end;

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

then A49: [x1,a] in R9 by A14, A47;
then [x1,x2] in R9 by A46, A17;
hence x1 <=_ R9,x2 by ARROW:def 4; :: thesis: x1 <> x2
assume x1 = x2 ; :: thesis: contradiction
hence contradiction by A48, A49, A46, A18; :: thesis: verum

end;

end;

end;

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

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

end;

end;

end;

card (Seg (card A1)) = card A1 by FINSEQ_1:57;
then f1 is onto by A36, FINSEQ_4:63;
then rng f1 = Seg (card A1) by FUNCT_2:def 3;
then dom (f1 ") = Seg (card A1) by A36, FUNCT_1:33;
then reconsider g1 = f1 " as FinSequence by FINSEQ_1:def 2;
A50: dom f1 = A by FUNCT_2:def 1;
then A51: rng g1 = A by A36, FUNCT_1:33;
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 A36, A50, FUNCT_1:33; :: 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
A52: n in dom g and
A53: m in dom g and
A54: n < m ; :: thesis: ( g /. n <> g /. m & [(g /. n),(g /. m)] in R )
reconsider gn = g . n as Element of A1 by A51, A52, FUNCT_1:def 3;
n in rng f by A36, A52, FUNCT_1:33;
then A55: n = f . gn by A36, FUNCT_1:35;
reconsider gm = g . m as Element of A1 by A51, A53, FUNCT_1:def 3;
A56: gm = g /. m by A53, PARTFUN1:def 6;
A57: m in rng f by A36, A53, FUNCT_1:33;
then m = f . gm by A36, FUNCT_1:35;
then A58: [gn,gm] in R by A37, A54, A55, ARROW:def 4;
gn = g /. n by A52, PARTFUN1:def 6;
hence ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) by A36, A54, A57, A55, A58, A56, FUNCT_1:35; :: thesis: verum

end;

end;