per cases ( A is empty or not A is empty ) ;
suppose A2: A is empty ; :: thesis: ex b1 being FinSequence of X st
( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. 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 b1 being FinSequence of X st
( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. 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 H1( set ) -> set = $1;
deffunc H2( Element of A1) -> set = { H1(x) where x is Element of A1 : ( x <=_ R9,$1 & x <> $1 ) } ;
deffunc H3( Element of A1) -> set = (card H2($1)) +^ 1;
A4: for x being Element of A1 holds H3(x) is Element of NAT
proof
let a be Element of A1; :: thesis: H3(a) is Element of NAT
defpred S1[ Element of A1] means ( $1 <=_ R9,a & $1 <> a );
{ H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch 1();
 then reconsider X = { H1(x) where x is Element of A1 : S1[x] } as finite set ;
reconsider n = card X as Element of NAT ;
n +^ 1 = n + 1 by CARD_2:36;
hence H3(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 = H3(x) from FUNCT_2:sch 9(A4);
A6: for x being Element of A1 holds not x in H2(x)
proof
let a be Element of A1; :: thesis: not a in H2(a)
assume a in H2(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 H2(x) c= A1
proof
let a be Element of A1; :: thesis: H2(a) c= A1
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H2(a) or y in A1 )
assume y in H2(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 S1[ Element of A1] means ( $1 <=_ R9,x2 & $1 <> x2 );
{ H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch 1();
 then reconsider Vx2 = H2(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 S1[ Element of A1] means ( $1 <=_ R9,x19 & $1 <> x19 );
{ H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch 1();
 then reconsider Vx1 = H2(x19) as finite set ;
defpred S2[ Element of A1] means ( $1 <=_ R9,x29 & $1 <> x29 );
{ H1(x) where x is Element of A1 : S2[x] } is finite from PRE_CIRC:sch 1();
 then reconsider Vx2 = H2(x29) as finite set ;
A22: for x1, x2 being Element of A1 st x1 <=_ R |_2 A,x2 holds
H2(x1) c= H2(x2)
proof
let x1, x2 be Element of A1; :: thesis: ( x1 <=_ R |_2 A,x2 implies H2(x1) c= H2(x2) )
assume x1 <=_ R |_2 A,x2 ; :: thesis: H2(x1) c= H2(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 H2(x1) or x in H2(x2) )
assume x in H2(x1) ; :: thesis: x in H2(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 H2(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 H2(x2)
proof
let x1, x2 be Element of A1; :: thesis: ( x1 <> x2 & x1 <=_ R |_2 A,x2 implies x1 in H2(x2) )
assume A32: x1 <> x2 ; :: thesis: ( not x1 <=_ R |_2 A,x2 or x1 in H2(x2) )
assume x1 <=_ R |_2 A,x2 ; :: thesis: x1 in H2(x2)
then [x1,x2] in R |_2 A by ARROW:def 4;
then x1 <=_ R9,x2 by A13, ARROW:def 4;
hence x1 in H2(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;
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 S1[ Element of A1] means ( $1 <=_ R9,x1 & $1 <> x1 );
{ H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch 1();
 then reconsider Vx1 = H2(x1) as finite set ;
defpred S2[ Element of A1] means ( $1 <=_ R9,x2 & $1 <> x2 );
{ H1(x) where x is Element of A1 : S2[x] } is finite from PRE_CIRC:sch 1();
 then reconsider Vx2 = H2(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;