per cases ;

suppose A2: A is empty ; :: thesis:

take <*> X ; :: thesis:
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:

end;

suppose A3: not A is empty ; :: thesis:

then reconsider X' = X as non empty set ;
reconsider A' = A as non empty finite Subset of X' by A3;
reconsider R' = R as Order of X' ;
[#] A = A ;
then reconsider A1 = A' as non empty finite Subset of RelStr(# A',(R' |_2 A') #) ;
A4: field (R' |_2 A') = A by ORDERS_1:100;
R is_connected_in A by A1, ORDERS_1:def 8;
then R |_2 A is connected by ORDERS_1:185;
then A5: R |_2 A is_connected_in A by A4, RELAT_2:def 14;
deffunc H₁( Element of A1) -> Element of NAT = (card (InitSegm A1,$1)) + 1;
consider f being Function of A1,NAT such that
A6: for x being Element of A1 holds f . x = H₁(x) from FUNCT_2:sch 4();
rng f c= Seg (card A1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x1 being set such that
A7: ( x1 in dom f & y = f . x1 ) by FUNCT_1:def 5;
reconsider x2 = x1 as Element of A1 by A7;
A8: card (InitSegm A1,x2) <= card A1 by NAT_1:44;
InitSegm A1,x2 <> A1 by ORDERS_2:62;
then card (InitSegm A1,x2) <> card A1 by Th3;
then card (InitSegm A1,x2) < card A1 by A8, XXREAL_0:1;
then A9: (card (InitSegm A1,x2)) + 1 <= card A1 by NAT_1:13;
A10: y = (card (InitSegm A1,x2)) + 1 by A6, A7;
reconsider y1 = y as Nat by A7;
0 + 1 <= y1 by A10, XREAL_1:8;
hence y in Seg (card A1) by A9, A10, FINSEQ_1:3; :: thesis:

end;

then reconsider f1 = f as Function of A1,(Seg (card A1)) by FUNCT_2: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:
assume A11: ( x1 in A1 & x2 in A1 & f . x1 = f . x2 ) ; :: thesis:
then reconsider x1' = x1 as Element of A1 ;
reconsider x2' = x2 as Element of A1 by A11;
f . x1' = (card (InitSegm A1,x1')) + 1 by A6;
then A12: (card (InitSegm A1,x1')) + 1 = (card (InitSegm A1,x2')) + 1 by A6, A11;

now

per cases ;

suppose x1' = x2' ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

suppose A13: x1' <> x2' ; :: thesis:

then A14: ( [x1',x2'] in R |_2 A or [x2',x1'] in R |_2 A ) by A5, RELAT_2:def 6;

A15: now

per cases by A14, ORDERS_2:def 9;

suppose x1' <= x2' ; :: thesis:

then x1' < x2' by A13, ORDERS_2:def 10;
hence InitSegm A1,x1' = InitSegm A1,x2' by A12, Th3, ORDERS_2:64; :: thesis:

end;

suppose x2' <= x1' ; :: thesis:

then x2' < x1' by A13, ORDERS_2:def 10;
hence InitSegm A1,x1' = InitSegm A1,x2' by A12, Th3, ORDERS_2:64; :: thesis:

end;

now

assume A16: x1' <> x2' ; :: thesis:
then A17: ( [x1',x2'] in R |_2 A or [x2',x1'] in R |_2 A ) by A5, RELAT_2:def 6;

per cases by A17, ORDERS_2:def 9;

suppose x1' <= x2' ; :: thesis:

then x1' < x2' by A16, ORDERS_2:def 10;
then x1' in InitSegm A1,x2' by ORDERS_2:57;
hence contradiction by A15, ORDERS_2:62; :: thesis:

end;

suppose x2' <= x1' ; :: thesis:

then x2' < x1' by A16, ORDERS_2:def 10;
then x2' in InitSegm A1,x1' by ORDERS_2:57;
hence contradiction by A15, ORDERS_2:62; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then A18: f1 is one-to-one by FUNCT_2:25;
card (Seg (card A1)) = card A1 by FINSEQ_1:78;
then A19: rng f1 = Seg (card A1) by A18, FINSEQ_4:78;
then dom (f1 " ) = Seg (card A1) by A18, FUNCT_1:55;
then reconsider g1 = f1 " as FinSequence by FINSEQ_1:def 2;
A20: dom f1 = A by FUNCT_2:def 1;
then A21: ( rng g1 = A & dom g1 = Seg (card A1) ) by A18, A19, FUNCT_1:55;
then reconsider g = g1 as FinSequence of X by FINSEQ_1:def 4;
take g ; :: thesis:
thus rng g = A by A18, A20, FUNCT_1:55; :: thesis:
A22: for x1, x2 being Element of A1 st f . x1 < f . x2 holds
x1 < x2

proof

let x1, x2 be Element of A1; :: thesis:
assume A23: f . x1 < f . x2 ; :: thesis:
A24: ( card (card (InitSegm A1,x1)) = card (InitSegm A1,x1) & card (card (InitSegm A1,x2)) = card (InitSegm A1,x2) ) ;
reconsider Cx1 = card (InitSegm A1,x1) as Cardinal ;
reconsider Cx2 = card (InitSegm A1,x2) as Cardinal ;
f . x1 = (card (InitSegm A1,x1)) + 1 by A6;
then (card (InitSegm A1,x1)) + 1 < (card (InitSegm A1,x2)) + 1 by A6, A23;
then ((card (InitSegm A1,x1)) + 1) - 1 < ((card (InitSegm A1,x2)) + 1) - 1 by XREAL_1:11;
then Cx1 in Cx2 by A24, NAT_1:42;
then (InitSegm A1,x2) \ (InitSegm A1,x1) <> {} by CARD_2:4;
then consider a being set such that
A25: a in (InitSegm A1,x2) \ (InitSegm A1,x1) by XBOOLE_0:def 1;
A26: ( a in InitSegm A1,x2 & not a in InitSegm A1,x1 ) by A25, XBOOLE_0:def 5;
reconsider a = a as Element of A1 by A25;
A27: ( a < x2 & not a < x1 ) by A26, ORDERS_2:57;

now

per cases by A27, ORDERS_2:def 10;

suppose not a <= x1 ; :: thesis:

then A28: not [a,x1] in R |_2 A by ORDERS_2:def 9;

now

per cases ;

suppose x1 = a ; :: thesis:

hence x1 < x2 by A26, ORDERS_2:57; :: thesis:

end;

suppose x1 <> a ; :: thesis:

then [x1,a] in R |_2 A by A5, A28, RELAT_2:def 6;
then x1 <= a by ORDERS_2:def 9;
hence x1 < x2 by A27, ORDERS_2:32; :: thesis:

end;

hence x1 < x2 ; :: thesis:

end;

suppose a = x1 ; :: thesis:

hence x1 < x2 by A26, ORDERS_2:57; :: thesis:

end;

hence x1 < x2 ; :: thesis:

end;

let n, m be Nat; :: thesis:
assume A29: ( n in dom g & m in dom g & n < m ) ; :: thesis:
then A30: ( n in rng f & m in rng f ) by A18, FUNCT_1:55;
reconsider gn = g . n as Element of A1 by A21, A29, FUNCT_1:def 5;
reconsider gm = g . m as Element of A1 by A21, A29, FUNCT_1:def 5;
A31: ( n = f . gn & m = f . gm ) by A18, A30, FUNCT_1:57;
then gn < gm by A22, A29;
then A32: ( gn <> gm & gn <= gm ) by ORDERS_2:def 10;
A33: R |_2 A c= R by XBOOLE_1:17;
A34: [gn,gm] in R |_2 A by A32, ORDERS_2:def 9;
( gn = g /. n & gm = g /. m ) by A29, PARTFUN1:def 8;
hence ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) by A29, A31, A33, A34; :: thesis:

end;