defpred S₁[ set ] means ex s being one-to-one FinSequence st
( rng s = $1 & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) );
A2: S₁[ {} ]

proof

reconsider s = {} as one-to-one FinSequence ;
take s ; :: thesis: ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) )
thus ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) ) ; :: thesis: verum

end;

AA: for A being Subset of F₁() st ( for B being set st B c< A holds
S₁[B] ) holds
S₁[A]

proof

let A be Subset of F₁(); :: thesis: ( ( for B being set st B c< A holds
S₁[B] ) implies S₁[A] )
assume Z0: for B being set st B c< A holds
S₁[B] ; :: thesis: S₁[A]

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

suppose A is empty ; :: thesis: S₁[A]

hence S₁[A] by A2; :: thesis: verum

end;

suppose not A is empty ; :: thesis: S₁[A]

then reconsider A9 = A as non empty finite set ;
W1: for x, y being set st x in A9 & y in A9 & P₁[x,y] holds
not P₁[y,x] by P1;
W2: for x, y, z being set st x in A9 & y in A9 & z in A9 & P₁[x,y] & P₁[y,z] holds
P₁[x,z] by P2;
consider x being set such that
W3: ( x in A9 & ( for y being set st y in A9 holds
not P₁[y,x] ) ) from ABCMIZ_A:sch 1(W1, W2);
set B = A \ {x};
B0: ( x nin A \ {x} & A \ {x} c= A ) by XBOOLE_1:36, ZFMISC_1:64;
then A \ {x} c< A by W3, XBOOLE_0:def 8;
then consider s being one-to-one FinSequence such that
B1: rng s = A \ {x} and
B2: for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j by Z0;
( <*x*> is one-to-one & rng <*x*> = {x} & {x} misses A \ {x} ) by XBOOLE_1:79, FINSEQ_1:56, FINSEQ_3:102;
then reconsider s9 = <*x*> ^ s as one-to-one FinSequence by B1, FINSEQ_3:98;
B3: {x} c= A by W3, ZFMISC_1:37;
B4: len <*x*> = 1 by FINSEQ_1:57;
thus S₁[A] :: thesis: verum

proof

take s9 ; :: thesis: ( rng s9 = A & ( for i, j being Nat st i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] holds
i < j ) )
thus rng s9 = (rng <*x*>) \/ (rng s) by FINSEQ_1:44
.= {x} \/ (A \ {x}) by B1, FINSEQ_1:55
.= A by B3, XBOOLE_1:45 ; :: thesis: for i, j being Nat st i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] holds
i < j
let i, j be Nat; :: thesis: ( i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] implies i < j )
assume C1: ( i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] ) ; :: thesis: i < j
C4: dom <*x*> = Seg 1 by FINSEQ_1:55;

per cases ( ( i in dom <*x*> & j in dom <*x*> ) or ( i in dom <*x*> & ex n being Nat st
( n in dom s & j = 1 + n ) ) or ( j in dom <*x*> & ex n being Nat st
( n in dom s & i = 1 + n ) ) or ( ex n being Nat st
( n in dom s & i = 1 + n ) & ex n being Nat st
( n in dom s & j = 1 + n ) ) ) by B4, C1, FINSEQ_1:38;

suppose ( i in dom <*x*> & j in dom <*x*> ) ; :: thesis: i < j

then ( i = 1 & j = 1 ) by C4, TARSKI:def 1, FINSEQ_1:4;
then ( s9 . i = x & s9 . j = x ) by FINSEQ_1:58;
hence i < j by W3, C1; :: thesis: verum

end;

suppose D1: ( i in dom <*x*> & ex n being Nat st
( n in dom s & j = 1 + n ) ) ; :: thesis: i < j

then D2: i = 1 by C4, TARSKI:def 1, FINSEQ_1:4;
consider n being Nat such that
D3: ( n in dom s & j = 1 + n ) by D1;
1 <= n by D3, FINSEQ_3:27;
hence i < j by D2, NAT_1:13, D3; :: thesis: verum

end;

suppose D1: ( j in dom <*x*> & ex n being Nat st
( n in dom s & i = 1 + n ) ) ; :: thesis: i < j

then j = 1 by C4, TARSKI:def 1, FINSEQ_1:4;
then D3: s9 . j = x by FINSEQ_1:58;
consider n being Nat such that
D4: ( n in dom s & i = 1 + n ) by D1;
s9 . i = s . n by B4, D4, FINSEQ_1:def 7;
then s9 . i in rng s by D4, FUNCT_1:def 5;
hence i < j by W3, C1, D3, B0, B1; :: thesis: verum

end;

suppose ( ex n being Nat st
( n in dom s & i = 1 + n ) & ex n being Nat st
( n in dom s & j = 1 + n ) ) ; :: thesis: i < j

then consider ni, nj being Nat such that
E1: ( ni in dom s & i = 1 + ni & nj in dom s & j = 1 + nj ) ;
( s9 . i = s . ni & s9 . j = s . nj ) by B4, E1, FINSEQ_1:def 7;
then ni < nj by B2, C1, E1;
hence i < j by E1, XREAL_1:8; :: thesis: verum

end;

end;

end;

end;

end;

end;

thus S₁[F₁()] from ABCMIZ_A:sch 2(AA); :: thesis: verum